# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1276483105 -7200
# Node ID 8ddf1330f2edf4595f7f5184f7873ccbc1f0d992
# Parent  d1ab5d2d6926b6dc5852de0ef64754df241fb134
completed proof and started section about respectfulness and preservation

diff -r d1ab5d2d6926 -r 8ddf1330f2ed Nominal/FSet.thy
--- a/Nominal/FSet.thy	Sun Jun 13 20:54:50 2010 +0200
+++ b/Nominal/FSet.thy	Mon Jun 14 04:38:25 2010 +0200
@@ -6,7 +6,7 @@
 *)
 
 theory FSet
-imports Quotient_List
+imports Quotient_List Quotient_Product
 begin
 
 text {* Definiton of List relation and the quotient type *}
@@ -1626,6 +1626,33 @@
 *}
 
 ML {*
+let
+val parser = Args.context -- Scan.lift Args.name_source
+fun typ_pat (ctxt, str) =
+str |> Syntax.parse_typ ctxt
+|> ML_Syntax.print_typ
+|> ML_Syntax.atomic
+in
+ML_Antiquote.inline "typ_pat" (parser >> typ_pat)
+end
+*}
+
+ML {*
+  mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}
+  |> Syntax.check_term @{context}
+  |> fastype_of
+  |> Syntax.string_of_typ @{context}
+  |> warning
+*}
+
+ML {*
+  mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}
+  |> Syntax.check_term @{context}
+  |> Syntax.string_of_term @{context}
+  |> warning
+*}
+
+ML {*
   absrep_fun AbsF @{context} (@{typ "('a list) list \<Rightarrow> 'a list"}, @{typ "('a fset) fset \<Rightarrow> 'a fset"})
   |> Syntax.string_of_term @{context}
   |> writeln
diff -r d1ab5d2d6926 -r 8ddf1330f2ed Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Sun Jun 13 20:54:50 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 04:38:25 2010 +0200
@@ -92,7 +92,9 @@
   An area where quotients are ubiquitous is reasoning about programming language
   calculi. A simple example is the lambda-calculus, whose raw terms are defined as
 
-  @{text [display, indent=10] "t ::= x | t t | \<lambda>x.t"}
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "t ::= x | t t | \<lambda>x.t"}\hfill\numbered{lambda}
+  \end{isabelle}
 
   \noindent
   The problem with this definition arises when one attempts to
@@ -116,7 +118,7 @@
   Nominal Isabelle, then manual reasoning is not an option.
 
   The purpose of a \emph{quotient package} is to ease the lifting of theorems
-  and automate the definitions and reasoning as much as possible. In the
+  and automate the reasoning as much as possible. In the
   context of HOL, there have been a few quotient packages already
   \cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier
   \cite{Homeier05} implemented in HOL4.  The fundamental construction these
@@ -148,40 +150,42 @@
   \end{center}
 
   \noindent
-  The starting point is an existing type, often referred to as the \emph{raw
-  type}, over which an equivalence relation given by the user is defined. With
-  this input the package introduces a new type, to which we refer as the
-  \emph{quotient type}. This type comes with an \emph{abstraction} and a
-  \emph{representation} function, written @{text Abs} and @{text
-  Rep}.\footnote{Actually slightly more basic functions are given; the @{text Abs}
-  and @{text Rep} need to be derived from them. We will show the details
-  later. } These functions relate elements in the existing type to ones in the
-  new type and vice versa; they can be uniquely identified by their type. For
-  example for the integer quotient construction the types of @{text Abs} and
-  @{text Rep} are
+  The starting point is an existing type, to which we often refer as the
+  \emph{raw type}, over which an equivalence relation given by the user is
+  defined. With this input the package introduces a new type, to which we
+  refer as the \emph{quotient type}. This type comes with an
+  \emph{abstraction} and a \emph{representation} function, written @{text Abs}
+  and @{text Rep}.\footnote{Actually slightly more basic functions are given;
+  the functions @{text Abs} and @{text Rep} need to be derived from them. We
+  will show the details later. } These functions relate elements in the
+  existing type to ones in the new type and vice versa; they can be uniquely
+  identified by their type. For example for the integer quotient construction
+  the types of @{text Abs} and @{text Rep} are
+
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   @{text "Abs :: nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep :: int \<Rightarrow> nat \<times> nat"}
   \end{isabelle}
 
   \noindent
-  However we often leave this typing information implicit for better
-  readability, but sometimes write @{text Abs_int} and @{text Rep_int} if the
-  typing information is important. Every abstraction and representation
-  function stands for an isomorphism between the non-empty subset and elements
-  in the new type. They are necessary for making definitions involving the new
-  type. For example @{text "0"} and @{text "1"} of type @{typ int} can be
-  defined as
+  We therefore often write @{text Abs_int} and @{text Rep_int} if the
+  typing information is important. 
+
+  Every abstraction and representation function stands for an isomorphism
+  between the non-empty subset and elements in the new type. They are
+  necessary for making definitions involving the new type. For example @{text
+  "0"} and @{text "1"} of type @{typ int} can be defined as
+
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  @{text "0 \<equiv> Abs (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs (1, 0)"}
+  @{text "0 \<equiv> Abs_int (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs_int (1, 0)"}
   \end{isabelle}
 
   \noindent
   Slightly more complicated is the definition of @{text "add"} having type 
   @{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition is as follows
 
-  @{text [display, indent=10] "add n m \<equiv> Abs (add_pair (Rep n) (Rep m))"}
+  @{text [display, indent=10] "add n m \<equiv> Abs_int (add_pair (Rep_int n) (Rep_int m))"}
   
   \noindent
   where we take the representation of the arguments @{text n} and @{text m},
@@ -203,9 +207,8 @@
 
   \noindent
   The quotient package should provide us with a definition for @{text "\<Union>"} in
-  terms of @{text flat}, @{text Rep} and @{text Abs} (the latter two having
-  the type @{text "\<alpha> fset \<Rightarrow> \<alpha> list"} and @{text "\<alpha> list \<Rightarrow> \<alpha> fset"},
-  respectively). The problem is that the method  used in the existing quotient
+  terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is 
+  that the method  used in the existing quotient
   packages of just taking the representation of the arguments and then take
   the abstraction of the result is \emph{not} enough. The reason is that case in case
   of @{text "\<Union>"} we obtain the incorrect definition
@@ -305,16 +308,18 @@
   option, \ldots) are described in Homeier, and we assume that @{text "map"}
   is the function that returns a map for a given type.
 
+  {\it say something about our use of @{text "\<sigma>s"}}
+
 *}
 
 section {* Quotient Types and Quotient Definitions\label{sec:type} *}
 
 text {*
   The first step in a quotient constructions is to take a name for the new
-  type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation defined over a
-  raw type, say @{text "\<sigma>"}. The equivalence relation for the quotient
-  construction, lets say @{text "R"}, must then be of type @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
-  bool"}. The user-visible part of the declaration is therefore 
+  type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},
+  defined over a raw type, say @{text "\<sigma>"}. The type of this equivalence
+  relation must be of type @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of
+  the declaration is therefore
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}
@@ -355,7 +360,7 @@
   \end{isabelle}
 
   \noindent 
-  and relating the new quotient type and equivalence classes of the raw
+  They relate the new quotient type and equivalence classes of the raw
   type. However, as Homeier \cite{Homeier05} noted, it is much more convenient
   to work with the following derived abstraction and representation functions
 
@@ -377,10 +382,10 @@
   \noindent
   holds (for the proof see \cite{Homeier05}).
 
-  The next step is to introduce new definitions involving the quotient type,
-  which need to be defined in terms of concepts of the raw type (remember this 
-  is the only way how toe be able to extend HOL with new definitions). For the
-  user visible is the declaration
+  The next step in a quotient construction is to introduce new definitions
+  involving the quotient type, which need to be defined in terms of concepts
+  of the raw type (remember this is the only way how to extend HOL
+  with new definitions). For the user visible is the declaration
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~~\isacommand{is}~~@{text "t :: \<sigma>"}
@@ -390,7 +395,7 @@
   where @{text t} is the definiens (its type @{text \<sigma>} can always be inferred)
   and @{text "c"} is the name of definiendum, whose type @{text "\<tau>"} needs to be
   given explicitly (the point is that @{text "\<tau>"} and @{text "\<sigma>"} can only differ 
-  in places where a quotient and raw type are involved). Two examples are
+  in places where a quotient and raw type are involved). Two concrete examples are
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -402,22 +407,24 @@
   
   \noindent
   The first one declares zero for integers and the second the operator for
-  building unions of finite sets. The problem for us is that from such
-  declarations we need to derive proper definitions using the @{text "Abs"}
-  and @{text "Rep"} functions for the quotient types involved. The data we
-  rely on is the given quotient type @{text "\<tau>"} and the raw type @{text "\<sigma>"}.
-  They allow us to define aggregate abstraction and representation functions
-  using the functions @{text "ABS (\<sigma>, \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose 
-  clauses are given below. The idea behind them is to recursively descend into 
-  both types and generate the appropriate @{text "Abs"} and @{text "Rep"} 
-  in places where the types differ. Therefore we returning just the identity
-  whenever the types are equal.
+  building unions of finite sets. 
+
+  The problem for us is that from such declarations we need to derive proper
+  definitions using the @{text "Abs"} and @{text "Rep"} functions for the
+  quotient types involved. The data we rely on is the given quotient type
+  @{text "\<tau>"} and the raw type @{text "\<sigma>"}.  They allow us to define aggregate
+  abstraction and representation functions using the functions @{text "ABS (\<sigma>,
+  \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses are given below. The idea behind
+  them is to recursively descend into types @{text \<sigma>} and @{text \<tau>}, and generate the appropriate
+  @{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore
+  we returning just the identity whenever the types are equal. All clauses
+  are as follows:
 
   \begin{center}
-  \begin{longtable}{rcl}
+  \begin{tabular}{rcl}
   \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ 
-  @{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\\
-  @{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\smallskip\\
+  @{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\
+  @{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\
   \multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\ 
   @{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
   @{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
@@ -425,54 +432,57 @@
   @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\
   @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\
   \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\
-  @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s')))"}\\
-  @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s'))) \<circ> Rep_\<kappa>\<^isub>q"}
-  \end{longtable}
+  @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s)))"}\\
+  @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s))) \<circ> Rep_\<kappa>\<^isub>q"}
+  \end{tabular}
   \end{center}
   %
   \noindent
   where in the last two clauses we have that the quotient type @{text "\<alpha>s
-  \<kappa>\<^isub>q"} is a quotient of the raw type @{text "\<rho>s \<kappa>"} (for example
+  \<kappa>\<^isub>q"} is the quotient of the raw type @{text "\<rho>s \<kappa>"} (for example
   @{text "int"} and @{text "nat \<times> nat"}, or @{text "\<alpha> fset"} and @{text "\<alpha>
   list"}). The quotient construction ensures that the type variables in @{text
   "\<rho>s"} must be amongst the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
-  matchers for the @{text "\<alpha>s"} when matching @{text "\<sigma>s \<kappa>\<^isub>q"} against
-  @{text "\<alpha>s \<kappa>\<^isub>q"}; similarly the @{text "\<tau>s'"} are given by the same
-  type-variables when matching @{text "\<tau>s \<kappa>"} against @{text "\<rho>s \<kappa>"}.  The
+  matchers for the @{text "\<alpha>s"} when matching @{text "\<rho>s \<kappa>"} against
+  @{text "\<sigma>s \<kappa>"}.  The
   function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw
   type as follows:
   %
   \begin{center}
-  \begin{longtable}{rcl}
+  \begin{tabular}{rcl}
   @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a\<^sup>\<alpha>"}\\
-  @{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id"}\\
+  @{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id :: \<kappa> \<Rightarrow> \<kappa>"}\\
   @{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\
   @{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>as. MAP'(\<sigma>)"}  
-  \end{longtable}
+  \end{tabular}
   \end{center}
   %
   \noindent
   In this definition we abuse the fact that we can interpret type-variables @{text \<alpha>} as 
-  term variables @{text a}, and in the last clause build an abstraction over all
-  term-variables inside the aggregate map-function generated by @{text "MAP'"}.
-  This aggregate map-function is necessary if we build quotients, say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"},
-  out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}. In this case @{text MAP}
-  generates the aggregate map-function:
+  term variables @{text a}. In the last clause we build an abstraction over all
+  term-variables inside the aggregate map-function generated by the auxiliary function 
+  @{text "MAP'"}.
+  The need of aggregate map-functions can be appreciated if we build quotients, 
+  say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types of the form @{text "(\<alpha> list) \<times> \<beta>"}. 
+  In this case @{text MAP} generates the aggregate map-function:
 
   @{text [display, indent=10] "\<lambda>a b. map_prod (map a) b"}
   
   \noindent
-  Returning to our example about @{term "concat"} and @{term "fconcat"} which have the
-  types @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}. Feeding this
-  into @{text ABS} gives us the abstraction function:
+  which we need to define the aggregate abstraction and representation functions.
+  
+  To se how these definitions pan out in practise, let us return to our
+  example about @{term "concat"} and @{term "fconcat"}, where we have types
+  @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>
+  fset"}. Feeding them into @{text ABS} gives us the abstraction function
 
   @{text [display, indent=10] "(map (map id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map id"}
 
   \noindent
-  where we already performed some @{text "\<beta>"}-simplifications. In our
-  implementation we further simplify this by noticing the usual laws about
-  @{text "map"}s and @{text "id"}, namely @{term "map id = id"} and @{text "f
-  \<circ> id = id \<circ> f = f"}. This gives us the simplified abstraction function
+  after some @{text "\<beta>"}-simplifications. In our implementation we further
+  simplify this abstraction function employing the usual laws about @{text
+  "map"}s and @{text "id"}, namely @{term "map id = id"} and @{text "f \<circ> id =
+  id \<circ> f = f"}. This gives us the abstraction function
 
   @{text [display, indent=10] "(map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
 
@@ -483,16 +493,18 @@
 
   \noindent
   Note that by using the operator @{text "\<singlearr>"} we do not have to 
-  distinguish between arguments and results: teh representation and abstraction
-  functions are just inverses which we can combine using @{text "\<singlearr>"}.
-  So all our definitions are of the general form
+  distinguish between arguments and results: the representation and abstraction
+  functions are just inverses of each other, which we can combine using 
+  @{text "\<singlearr>"} to deal uniformly with arguments of functions and 
+  their result. As a result, all definitions in the quotient package 
+  are of the general form
 
   @{text [display, indent=10] "c \<equiv> ABS (\<sigma>, \<tau>) t"}
 
   \noindent
-  where @{text \<sigma>} is the type of @{text "t"} and @{text "\<tau>"} the type of the 
-  newly defined quotient constant @{text "c"}. To ensure we obtained a correct 
-  definition, we can prove:
+  where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the
+  type of the defined quotient constant @{text "c"}. To ensure we
+  obtained a correct definition, we can prove:
 
   \begin{lemma}
   If @{text "ABS (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"} 
@@ -502,19 +514,47 @@
   \end{lemma}
 
   \begin{proof}
-  By induction of the definitions of @{text "ABS"}, @{text "REP"} and @{text "MAP"}.
+  By induction and analysing the definitions of @{text "ABS"}, @{text "REP"} 
+  and @{text "MAP"}. The cases of equal and function types are straightforward
+  (the latter follows from @{text "\<singlearr>"} having the type
+  @{text "(\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> (\<gamma> \<Rightarrow> \<delta>) \<Rightarrow> (\<beta> \<Rightarrow> \<gamma>) \<Rightarrow> (\<alpha> \<Rightarrow> \<delta>)"}). The case of equal
+  type constructors follows by observing that a map-function after applying 
+  the functions @{text "ABS (\<sigma>s, \<tau>s)"} produce a term of type @{text "\<sigma>s \<kappa> \<Rightarrow> \<tau>s \<kappa>"}.
+  The interesting case is the one with unequal type constructors. Since we know the
+  quotient is between @{text "\<alpha>s \<kappa>\<^isub>q"} and @{text "\<rho>s \<kappa>"}, we have that @{text "Abs_\<kappa>\<^isub>q"}
+  is of type @{text "\<rho>s \<kappa> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"}, that can be more specialised to @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"}
+  where the type variables @{text "\<alpha>s"} are instantiated with @{text "\<tau>s"}. The 
+  complete type can be calculated by observing that @{text "MAP (\<rho>s \<kappa>)"} after applying
+  the functions @{text "ABS (\<sigma>s', \<tau>s)"} to it, returns a term of type 
+  @{text "\<rho>s[\<sigma>s'] \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}. This type is equivalent to  @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"} 
+  as desired.\qed
   \end{proof}
   
   \noindent
-  This lemma fails for the abstraction and representation functions used in,
-  for example, Homeier's quotient package.
+  The reader should note that this lemma fails for the abstraction and representation 
+  functions used, for example, in Homeier's quotient package.
 *}
 
-subsection {* Respectfulness *}
+section {* Respectfulness and Preservation *}
 
 text {*
+  Before we can lift theorems involving the raw types to theorems over
+  quotient types, we have to impose some restrictions. The reason is that not
+  all theorems can be lifted. Homeier formulates these restrictions in terms
+  of \emph{respectfullness} and \emph{preservation} of constants occuring in
+  theorems.
 
-  A respectfulness lemma for a constant states that the equivalence
+  The respectfulness property for a constant states that it essentially 
+  respects the equivalence relation involved in the quotient. An example
+  is the function returning bound variables of a lambda-term (see \eqref{lambda})
+  and @{text "\<alpha>"}-equivalence. It will turn out that this function is not 
+  respectful. 
+
+  To state the respectfulness property we have to define \emph{aggregate equivalence 
+  relations}.
+
+  @{text [display] "GIVE DEFINITION HERE"}
+
   class returned by this constant depends only on the equivalence
   classes of the arguments applied to the constant. To automatically
   lift a theorem that talks about a raw constant, to a theorem about
@@ -522,10 +562,10 @@
 
   A respectfulness condition for a constant can be expressed in
   terms of an aggregate relation between the constant and itself,
-  for example the respectfullness for @{term "append"}
+  for example the respectfullness for @{text "append"}
   can be stated as:
 
-  @{thm [display, indent=10] append_rsp[no_vars]}
+  @{text [display, indent=10] "(R \<doublearr> R \<doublearr> R) append append"}
 
   \noindent
   Which after unfolding the definition of @{term "op ===>"} is equivalent to:
@@ -573,7 +613,6 @@
 
 *}
 
-subsection {* Preservation *}
 
 text {*
   Sometimes a non-lifted polymorphic constant is instantiated to a
diff -r d1ab5d2d6926 -r 8ddf1330f2ed Quotient-Paper/document/root.tex
--- a/Quotient-Paper/document/root.tex	Sun Jun 13 20:54:50 2010 +0200
+++ b/Quotient-Paper/document/root.tex	Mon Jun 14 04:38:25 2010 +0200
@@ -41,7 +41,7 @@
 non-empty types. Both extensions are often performed in quotient
 constructions. To ease the work involved with such quotient constructions, we
 re-implemented in Isabelle/HOL the quotient package by Homeier. In doing so we
-extended his work in order to deal with compositions of quotients. Also, we
+extended his work in order to deal with compositions of quotients. We also
 designed our quotient package so that every step in a quotient construction
 can be performed separately and as a result we are able to specify completely
 the procedure of lifting theorems from the raw level to the quotient level.