diff -r 7412424213ec -r 49cc1af89de9 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Mon Jun 21 06:46:28 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Mon Jun 21 06:47:40 2010 +0100
@@ -1,5 +1,3 @@
-(* How to change the notation for \<lbrakk> \<rbrakk> meta-level implications? *)
-
 (*<*)
 theory Paper
 imports "Quotient"
@@ -7,22 +5,36 @@
         "../Nominal/FSet"
 begin
 
-print_syntax
+(****
+
+** things to do for the next version
+*
+* - what are quot_thms?
+* - what do all preservation theorems look like,
+    in particular preservation for quotient
+    compositions
+*)
 
 notation (latex output)
-  rel_conj ("_ OOO _" [53, 53] 52) and
-  "op -->" (infix "\<rightarrow>" 100) and
-  "==>" (infix "\<Rightarrow>" 100) and
-  fun_map (infix "\<longrightarrow>" 51) and
-  fun_rel (infix "\<Longrightarrow>" 51) and
+  rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
+  pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
+  "op -->" (infix "\<longrightarrow>" 100) and
+  "==>" (infix "\<Longrightarrow>" 100) and
+  fun_map ("_ \<^raw:\mbox{\singlearr}> _" 51) and
+  fun_rel ("_ \<^raw:\mbox{\doublearr}> _" 51) and
   list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
-  fempty ("\<emptyset>\<^isub>f") and
-  funion ("_ \<union>\<^isub>f _") and
-  Cons ("_::_") 
+  fempty ("\<emptyset>") and
+  funion ("_ \<union> _") and
+  finsert ("{_} \<union> _") and 
+  Cons ("_::_") and
+  concat ("flat") and
+  fconcat ("\<Union>")
+ 
   
 
 ML {*
 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;
+
 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
   let
     val concl =
@@ -32,13 +44,16 @@
     | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
   end);
 *}
+
 setup {*
   Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #>
   Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #>
   Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))
 *}
+
 (*>*)
 
+
 section {* Introduction *}
 
 text {* 
@@ -46,612 +61,1105 @@
   {\em ``Not using a [quotient] package has its advantages: we do not have to\\ 
     collect all the theorems we shall ever want into one giant list;''}\\
     Larry Paulson \cite{Paulson06}
-  \end{flushright}\smallskip
+  \end{flushright}
 
   \noindent
-  Isabelle is a generic theorem prover in which many logics can be
+  Isabelle is a popular generic theorem prover in which many logics can be
   implemented. The most widely used one, however, is Higher-Order Logic
   (HOL). This logic consists of a small number of axioms and inference rules
   over a simply-typed term-language. Safe reasoning in HOL is ensured by two
   very restricted mechanisms for extending the logic: one is the definition of
   new constants in terms of existing ones; the other is the introduction of
   new types by identifying non-empty subsets in existing types. It is well
-  understood how to use both mechanisms for dealing with quotient constructions in
-  HOL (see \cite{Homeier05,Paulson06}).  For example the integers
-  in Isabelle/HOL are constructed by a quotient construction over the type
-  @{typ "nat \<times> nat"} and the equivalence relation
+  understood how to use both mechanisms for dealing with quotient
+  constructions in HOL (see \cite{Homeier05,Paulson06}).  For example the
+  integers in Isabelle/HOL are constructed by a quotient construction over the
+  type @{typ "nat \<times> nat"} and the equivalence relation
 
-  @{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + n\<^isub>2 = m\<^isub>1 + m\<^isub>2"}
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + m\<^isub>2 = m\<^isub>1 + n\<^isub>2"}\hfill\numbered{natpairequiv}
+  \end{isabelle}
 
   \noindent
   This constructions yields the new type @{typ int} and definitions for @{text
-  "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of 
-  natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations 
-  such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined 
-  in terms of operations on pairs of natural numbers (namely @{text "add\<^bsub>nat\<times>nat\<^esub>
-  (x\<^isub>1, y\<^isub>1) (x\<^isub>2, y\<^isub>2) \<equiv> (x\<^isub>1 +
-  x\<^isub>2, y\<^isub>1 + y\<^isub>2)"}).  Similarly one can construct the
-  type of finite sets by quotienting lists according to the equivalence
-  relation
+  "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of
+  natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations
+  such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in
+  terms of operations on pairs of natural numbers (namely @{text
+  "add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2,
+  m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}).
+  Similarly one can construct the type of finite sets, written @{term "\<alpha> fset"}, 
+  by quotienting the type @{text "\<alpha> list"} according to the equivalence relation
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}\hfill\numbered{listequiv}
+  \end{isabelle}
 
-  @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}
+  \noindent
+  which states that two lists are equivalent if every element in one list is
+  also member in the other. The empty finite set, written @{term "{||}"}, can
+  then be defined as the empty list and the union of two finite sets, written
+  @{text "\<union>"}, as list append.
+
+  Quotients are important in a variety of areas, but they are really ubiquitous in
+  the area of reasoning about programming language calculi. A simple example
+  is the lambda-calculus, whose raw terms are defined as
+
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "t ::= x | t t | \<lambda>x.t"}\hfill\numbered{lambda}
+  \end{isabelle}
 
   \noindent
-  which states that two lists are equivalent if every element in one list is also
-  member in the other (@{text "\<in>"} stands here for membership in lists). The
-  empty finite set, written @{term "{||}"} can then be defined as the 
-  empty list and union of two finite sets, written @{text "\<union>\<^isub>f"}, as list append. 
+  The problem with this definition arises, for instance, when one attempts to
+  prove formally the substitution lemma \cite{Barendregt81} by induction
+  over the structure of terms. This can be fiendishly complicated (see
+  \cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof
+  about raw lambda-terms). In contrast, if we reason about
+  $\alpha$-equated lambda-terms, that means terms quotient according to
+  $\alpha$-equivalence, then the reasoning infrastructure provided, 
+  for example, by Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal 
+  proof of the substitution lemma almost trivial. 
 
-  Another important area of quotients is reasoning about programming language
-  calculi. A simple example are lambda-terms defined as
+  The difficulty is that in order to be able to reason about integers, finite
+  sets or $\alpha$-equated lambda-terms one needs to establish a reasoning
+  infrastructure by transferring, or \emph{lifting}, definitions and theorems
+  from the raw type @{typ "nat \<times> nat"} to the quotient type @{typ int}
+  (similarly for finite sets and $\alpha$-equated lambda-terms). This lifting
+  usually requires a \emph{lot} of tedious reasoning effort \cite{Paulson06}.  
+  It is feasible to do this work manually, if one has only a few quotient
+  constructions at hand. But if they have to be done over and over again, as in 
+  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 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
+  quotient packages perform can be illustrated by the following picture:
 
   \begin{center}
-  @{text "t ::= x | t t | \<lambda>x.t"}
+  \mbox{}\hspace{20mm}\begin{tikzpicture}
+  %%\draw[step=2mm] (-4,-1) grid (4,1);
+  
+  \draw[very thick] (0.7,0.3) circle (4.85mm);
+  \draw[rounded corners=1mm, very thick] ( 0.0,-0.9) rectangle ( 1.8, 0.9);
+  \draw[rounded corners=1mm, very thick] (-1.95,0.8) rectangle (-2.9,-0.195);
+  
+  \draw (-2.0, 0.8) --  (0.7,0.8);
+  \draw (-2.0,-0.195)  -- (0.7,-0.195);
+
+  \draw ( 0.7, 0.23) node {\begin{tabular}{@ {}c@ {}}equiv-\\[-1mm]clas.\end{tabular}};
+  \draw (-2.45, 0.35) node {\begin{tabular}{@ {}c@ {}}new\\[-1mm]type\end{tabular}};
+  \draw (1.8, 0.35) node[right=-0.1mm]
+    {\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw elements)\end{tabular}};
+  \draw (0.9, -0.55) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
+  
+  \draw[->, very thick] (-1.8, 0.36) -- (-0.1,0.36);
+  \draw[<-, very thick] (-1.8, 0.16) -- (-0.1,0.16);
+  \draw (-0.95, 0.26) node[above=0.4mm] {@{text Rep}};
+  \draw (-0.95, 0.26) node[below=0.4mm] {@{text Abs}};
+
+  \end{tikzpicture}
   \end{center}
 
   \noindent
-  The difficulty with this definition of lambda-terms arises when, for 
-  example, proving formally the substitution lemma ...
-  On the other hand if we reason about alpha-equated lambda-terms, that means
-  terms quotient according to alpha-equivalence, then reasoning infrastructure
-  can be introduced that make the formal proof of the substitution lemma
-  almost trivial. 
+  The starting point is an existing type, to which we refer as the
+  \emph{raw type} and 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. } They relate elements in the
+  existing type to elements in the new type and vice versa, and can be uniquely
+  identified by their quotient 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
+  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
 
 
-  The problem is that in order to be able to reason about integers, finite sets
-  and alpha-equated lambda-terms one needs to establish a reasoning infrastructure by
-  transferring, or \emph{lifting}, definitions and theorems from the ``raw''
-  type @{typ "nat \<times> nat"} to the quotient type @{typ int} (similarly for
-  @{text "\<alpha> list"} and finite sets of type @{text "\<alpha>"}, and also for raw lambda-terms
-  and alpha-equated lambda-terms). This lifting usually
-  requires a \emph{lot} of tedious reasoning effort.  The purpose of a \emph{quotient
-  package} is to ease the lifting and automate the reasoning as much as
-  possible. While for integers and finite sets teh tedious reasoning needs
-  to be done only once, Nominal Isabelle providing a reasoning infrastructure 
-  for binders and @{text "\<alpha>"}-equated terms it needs to be done over and over 
-  again.
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{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
 
-  Such a package is a central component of the new version of
-  Nominal Isabelle where representations of alpha-equated terms are
-  constructed according to specifications given by the user.
+   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "add n m \<equiv> Abs_int (add_pair (Rep_int n) (Rep_int m))"}
+  \hfill\numbered{adddef}
+  \end{isabelle}
 
-  
-  In the context of HOL, there have been several quotient packages (...). The
-  most notable is the one by Homeier (...) implemented in HOL4. However, what is
-  surprising, none of them can deal compositions of quotients, for example with 
-  lifting theorems about @{text "concat"}:
+  \noindent
+  where we take the representation of the arguments @{text n} and @{text m},
+  add them according to the function @{text "add_pair"} and then take the
+  abstraction of the result.  This is all straightforward and the existing
+  quotient packages can deal with such definitions. But what is surprising
+  that none of them can deal with slightly more complicated definitions involving
+  \emph{compositions} of quotients. Such compositions are needed for example
+  in case of quotienting lists to yield finite sets and the operator that 
+  flattens lists of lists, defined as follows
 
-  @{thm [display] concat.simps(1)}
-  @{thm [display] concat.simps(2)[no_vars]}
+  @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]}
 
   \noindent
-  One would like to lift this definition to the operation:
+  We expect that the corresponding operator on finite sets, written @{term "fconcat"},
+  builds finite unions of finite sets:
+
+  @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
+
+  \noindent
+  The quotient package should automatically provide us with a definition for @{text "\<Union>"} in
+  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 taking
+  the abstraction of the result is \emph{not} enough. The reason is that in case
+  of @{text "\<Union>"} we obtain the incorrect definition
 
-  @{thm [display] fconcat_empty[no_vars]}
-  @{thm [display] fconcat_insert[no_vars]}
+  @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}
+
+  \noindent
+  where the right-hand side is not even typable! This problem can be remedied in the
+  existing quotient packages by introducing an intermediate step and reasoning
+  about flattening of lists of finite sets. However, this remedy is rather
+  cumbersome and inelegant in light of our work, which can deal with such
+  definitions directly. The solution is that we need to build aggregate
+  representation and abstraction functions, which in case of @{text "\<Union>"}
+  generate the following definition
+
+  @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat ((map Rep_fset \<circ> Rep_fset) S))"}
 
   \noindent
-  What is special about this operation is that we have as input
-  lists of lists which after lifting turn into finite sets of finite
-  sets.
+  where @{term map} is the usual mapping function for lists. In this paper we
+  will present a formal definition of our aggregate abstraction and
+  representation functions (this definition was omitted in \cite{Homeier05}). 
+  They generate definitions, like the one above for @{text "\<Union>"}, 
+  according to the type of the raw constant and the type
+  of the quotient constant. This means we also have to extend the notions
+  of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}
+  from Homeier \cite{Homeier05}.
+
+  In addition we are able to address the criticism by Paulson \cite{Paulson06} cited
+  at the beginning of this section about having to collect theorems that are
+  lifted from the raw level to the quotient level into one giant list. Our
+  quotient package is the first one that is modular so that it allows to lift
+  single higher-order theorems separately. This has the advantage for the user of being able to develop a
+  formal theory interactively as a natural progression. A pleasing side-result of
+  the modularity is that we are able to clearly specify what is involved
+  in the lifting process (this was only hinted at in \cite{Homeier05} and
+  implemented as a ``rough recipe'' in ML-code).
+
+
+  The paper is organised as follows: Section \ref{sec:prelims} presents briefly
+  some necessary preliminaries; Section \ref{sec:type} describes the definitions 
+  of quotient types and shows how definitions of constants can be made over 
+  quotient types. Section \ref{sec:resp} introduces the notions of respectfulness
+  and preservation; Section \ref{sec:lift} describes the lifting of theorems;
+  Section \ref{sec:examples} presents some examples
+  and Section \ref{sec:conc} concludes and compares our results to existing 
+  work.
 *}
 
-subsection {* Contributions *}
+section {* Preliminaries and General Quotients\label{sec:prelims} *}
 
 text {*
-  We present the detailed lifting procedure, which was not shown before.
+  We give in this section a crude overview of HOL and describe the main
+  definitions given by Homeier for quotients \cite{Homeier05}.
+
+  At its core, HOL is based on a simply-typed term language, where types are 
+  recorded in Church-style fashion (that means, we can always infer the type of 
+  a term and its subterms without any additional information). The grammars
+  for types and terms are as follows
 
-  The quotient package presented in this paper has the following
-  advantages over existing packages:
-  \begin{itemize}
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}rl@ {\hspace{3mm}}l@ {}}
+  @{text "\<sigma>, \<tau> ::="} & @{text "\<alpha> | (\<sigma>,\<dots>, \<sigma>) \<kappa>"} & (type variables and type constructors)\\
+  @{text "t, s ::="} & @{text "x\<^isup>\<sigma> | c\<^isup>\<sigma> | t t | \<lambda>x\<^isup>\<sigma>. t"} & 
+  (variables, constants, applications and abstractions)\\
+  \end{tabular}
+  \end{isabelle}
 
-  \item We define quotient composition, function map composition and
-    relation map composition. This lets lifting polymorphic types with
-    subtypes quotiented as well. We extend the notions of
-    respectfulness and preservation to cope with quotient
-    composition.
+  \noindent
+  We often write just @{text \<kappa>} for @{text "() \<kappa>"}, and use @{text "\<alpha>s"} and
+  @{text "\<sigma>s"} to stand for collections of type variables and types,
+  respectively.  The type of a term is often made explicit by writing @{text
+  "t :: \<sigma>"}. HOL includes a type @{typ bool} for booleans and the function
+  type, written @{text "\<sigma> \<Rightarrow> \<tau>"}. HOL also contains many primitive and defined
+  constants; a primitive constant is equality, with type @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
+  bool"}, and the identity function with type @{text "id :: \<sigma> \<Rightarrow> \<sigma>"} is
+  defined as @{text "\<lambda>x\<^sup>\<sigma>. x\<^sup>\<sigma>"}).
 
-  \item We allow lifting only some occurrences of quotiented
-    types. Rsp/Prs extended. (used in nominal)
+  An important point to note is that theorems in HOL can be seen as a subset
+  of terms that are constructed specially (namely through axioms and proof
+  rules). As a result we are able to define automatic proof
+  procedures showing that one theorem implies another by decomposing the term
+  underlying the first theorem.
 
-  \item The quotient package is very modular. Definitions can be added
-    separately, rsp and prs can be proved separately, Quotients and maps
-    can be defined separately and theorems can
-    be lifted on a need basis. (useful with type-classes).
+  Like Homeier, our work relies on map-functions defined for every type
+  constructor taking some arguments, for example @{text map} for lists. Homeier
+  describes in \cite{Homeier05} map-functions for products, sums, options and
+  also the following map for function types
+
+  @{thm [display, indent=10] fun_map_def[no_vars, THEN eq_reflection]}
+
+  \noindent
+  Using this map-function, we can give the following, equivalent, but more 
+  uniform, definition for @{text add} shown in \eqref{adddef}:
+
+  @{text [display, indent=10] "add \<equiv> (Rep_int \<singlearr> Rep_int \<singlearr> Abs_int) add_pair"}
 
-  \item Can be used both manually (attribute, separate tactics,
-    rsp/prs databases) and programatically (automated definition of
-    lifted constants, the rsp proof obligations and theorem statement
-    translation according to given quotients).
+  \noindent
+  Using extensionality and unfolding the definition of @{text "\<singlearr>"}, 
+  we can get back to \eqref{adddef}. 
+  In what follows we shall use the convention to write @{text "map_\<kappa>"} for a map-function 
+  of the type-constructor @{text \<kappa>}. In our implementation we maintain 
+  a database of these map-functions that can be dynamically extended.
 
-  \end{itemize}
-*}
-
-section {* Quotient Type*}
-
+  It will also be necessary to have operators, referred to as @{text "rel_\<kappa>"},
+  which define equivalence relations in terms of constituent equivalence
+  relations. For example given two equivalence relations @{text "R\<^isub>1"}
+  and @{text "R\<^isub>2"}, we can define an equivalence relations over 
+  products as follows
+  %
+  @{text [display, indent=10] "(R\<^isub>1 \<tripple> R\<^isub>2) (x\<^isub>1, x\<^isub>2) (y\<^isub>1, y\<^isub>2) \<equiv> R\<^isub>1 x\<^isub>1 y\<^isub>1 \<and> R\<^isub>2 x\<^isub>2 y\<^isub>2"}
 
-
-text {*
-  In this section we present the definitions of a quotient that follow
-  those by Homeier, the proofs can be found there.
+  \noindent
+  Homeier gives also the following operator for defining equivalence 
+  relations over function types
+  %
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{thm fun_rel_def[of "R\<^isub>1" "R\<^isub>2", no_vars, THEN eq_reflection]}
+  \hfill\numbered{relfun}
+  \end{isabelle}
+  
+  \noindent
+  In the context of quotients, the following two notions from are \cite{Homeier05} 
+  needed later on.
 
-  \begin{definition}[Quotient]
-  A relation $R$ with an abstraction function $Abs$
-  and a representation function $Rep$ is a \emph{quotient}
-  if and only if:
+  \begin{definition}[Respects]\label{def:respects}
+  An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}.
+  \end{definition}
 
+  \begin{definition}[Bounded Quantification and Bounded Abstractions]\label{def:babs}
+  @{text "\<forall>x \<in> S. P x"} holds if for all @{text x}, @{text "x \<in> S"} implies @{text "P x"};
+  and @{text "(\<lambda>x \<in> S. f x) = f x"} provided @{text "x \<in> S"}.
+  \end{definition}
+
+  The central definition in Homeier's work \cite{Homeier05} relates equivalence 
+  relations, abstraction and representation functions:
+
+  \begin{definition}[Quotient Types]
+  Given a relation $R$, an abstraction function $Abs$
+  and a representation function $Rep$, the predicate @{term "Quotient R Abs Rep"}
+  means
   \begin{enumerate}
   \item @{thm (rhs1) Quotient_def[of "R", no_vars]}
   \item @{thm (rhs2) Quotient_def[of "R", no_vars]}
   \item @{thm (rhs3) Quotient_def[of "R", no_vars]}
   \end{enumerate}
-
   \end{definition}
 
-  \begin{definition}[Relation map and function map]\\
-  @{thm fun_rel_def[of "R1" "R2", no_vars]}\\
-  @{thm fun_map_def[no_vars]}
+  \noindent
+  The value of this definition is that validity of @{text "Quotient R Abs Rep"} can 
+  often be proved in terms of the validity of @{text "Quotient"} over the constituent 
+  types of @{text "R"}, @{text Abs} and @{text Rep}. 
+  For example Homeier proves the following property for higher-order quotient
+  types:
+ 
+  \begin{proposition}\label{funquot}
+  @{thm[mode=IfThen] fun_quotient[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2" 
+      and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]}
+  \end{proposition}
+
+  \noindent
+  As a result, Homeier is able to build an automatic prover that can nearly
+  always discharge a proof obligation involving @{text "Quotient"}. Our quotient
+  package makes heavy 
+  use of this part of Homeier's work including an extension 
+  to deal with compositions of equivalence relations defined as follows:
+
+  \begin{definition}[Composition of Relations]
+  @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate
+  composition defined by @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
+  holds if and only if @{thm (prem 1) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} and
+  @{thm (prem 2) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}.
   \end{definition}
 
-  The main theorems for building higher order quotients is:
-  \begin{lemma}[Function Quotient]
-  If @{thm (prem 1) fun_quotient[no_vars]} and @{thm (prem 2) fun_quotient[no_vars]}
-  then @{thm (concl) fun_quotient[no_vars]}
-  \end{lemma}
+  \noindent
+  Unfortunately, there are two predicaments with compositions of relations.
+  First, a general quotient theorem, like the one given in Proposition \ref{funquot},
+  cannot be stated inside HOL, because of the restriction on types.
+  Second, even if we were able to state such a quotient theorem, it
+  would not be true in general. However, we can prove specific instances of a
+  quotient theorem for composing particular quotient relations.
+  For example, to lift theorems involving @{term flat} the quotient theorem for 
+  composing @{text "\<approx>\<^bsub>list\<^esub>"} will be necessary: given @{term "Quotient R Abs Rep"} 
+  with @{text R} being an equivalence relation, then
 
+  @{text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep \<circ> rep_fset)"}
+
+  \vspace{-.5mm}
 *}
 
-subsection {* Higher Order Logic *}
-
-text {*
-
-  Types:
-  \begin{eqnarray}\nonumber
-  @{text "\<sigma> ::="} & @{text "\<alpha>"} & \textrm{(type variable)} \\ \nonumber
-      @{text "|"} & @{text "(\<sigma>,\<dots>,\<sigma>)\<kappa>"} & \textrm{(type construction)}
-  \end{eqnarray}
-
-  Terms:
-  \begin{eqnarray}\nonumber
-  @{text "t ::="} & @{text "x\<^isup>\<sigma>"} & \textrm{(variable)} \\ \nonumber
-      @{text "|"} & @{text "c\<^isup>\<sigma>"} & \textrm{(constant)} \\ \nonumber
-      @{text "|"} & @{text "t t"} & \textrm{(application)} \\ \nonumber
-      @{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber
-  \end{eqnarray}
-
-*}
-
-section {* Constants *}
-
-(* Say more about containers? *)
+section {* Quotient Types and Quotient Definitions\label{sec:type} *}
 
 text {*
+  The first step in a quotient construction is to take a name for the new
+  type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},
+  defined over a raw type, say @{text "\<sigma>"}. The type of the equivalence
+  relation must be @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of
+  the quotient type declaration is therefore
 
-  To define a constant on the lifted type, an aggregate abstraction
-  function is applied to the raw constant. Below we describe the operation
-  that generates
-  an aggregate @{term "Abs"} or @{term "Rep"} function given the
-  compound raw type and the compound quotient type.
-  This operation will also be used in translations of theorem statements
-  and in the lifting procedure.
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}\hfill\numbered{typedecl}
+  \end{isabelle}
+
+  \noindent
+  and a proof that @{text "R"} is indeed an equivalence relation. Two concrete
+  examples are
+
+  
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  \isacommand{quotient\_type}~~@{text "int = nat \<times> nat / \<approx>\<^bsub>nat \<times> nat\<^esub>"}\\
+  \isacommand{quotient\_type}~~@{text "\<alpha> fset = \<alpha> list / \<approx>\<^bsub>list\<^esub>"}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  which introduce the type of integers and of finite sets using the
+  equivalence relations @{text "\<approx>\<^bsub>nat \<times> nat\<^esub>"} and @{text
+  "\<approx>\<^bsub>list\<^esub>"} defined in \eqref{natpairequiv} and
+  \eqref{listequiv}, respectively (the proofs about being equivalence
+  relations is omitted).  Given this data, we define for declarations shown in
+  \eqref{typedecl} the quotient types internally as
+  
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \isacommand{typedef}~~@{text "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>x. c = R x}"}
+  \end{isabelle}
+
+  \noindent
+  where the right-hand side is the (non-empty) set of equivalence classes of
+  @{text "R"}. The constraint in this declaration is that the type variables
+  in the raw type @{text "\<sigma>"} must be included in the type variables @{text
+  "\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will then provide us with the following
+  abstraction and representation functions 
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "abs_\<kappa>\<^isub>q :: \<sigma> set \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"}\hspace{10mm}@{text "rep_\<kappa>\<^isub>q :: \<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma> set"}
+  \end{isabelle}
+
+  \noindent 
+  As can be seen from the type, 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
 
-  The operation is additionally able to descend into types for which
-  maps are known. Such maps for most common types (list, pair, sum,
-  option, \ldots) are described in Homeier, and we assume that @{text "map"}
-  is the function that returns a map for a given type. Then REP/ABS is defined
-  as follows:
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "Abs_\<kappa>\<^isub>q x \<equiv> abs_\<kappa>\<^isub>q (R x)"}\hspace{10mm}@{text "Rep_\<kappa>\<^isub>q x \<equiv> \<epsilon> (rep_\<kappa>\<^isub>q x)"}
+  \end{isabelle}
+  
+  \noindent
+  on the expense of having to use Hilbert's choice operator @{text "\<epsilon>"} in the
+  definition of @{text "Rep_\<kappa>\<^isub>q"}. These derived notions relate the
+  quotient type and the raw type directly, as can be seen from their type,
+  namely @{text "\<sigma> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"},
+  respectively.  Given that @{text "R"} is an equivalence relation, the
+  following property holds  for every quotient type 
+  (for the proof see \cite{Homeier05}).
+
+  \begin{proposition}
+  @{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.
+  \end{proposition}
+
+  The next step in a quotient construction is to introduce definitions of new constants
+  involving the quotient type. These definitions need to be given in terms of concepts
+  of the raw type (remember this is the only way how to extend HOL
+  with new definitions). For the user the visible part of such definitions is the declaration
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~~\isacommand{is}~~@{text "t :: \<sigma>"}
+  \end{isabelle}
+
+  \noindent
+  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 is involved). Two concrete examples are
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0::nat, 0::nat)"}\\
+  \isacommand{quotient\_definition}~~@{text "\<Union> :: (\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}~~%
+  \isacommand{is}~~@{text "flat"} 
+  \end{tabular}
+  \end{isabelle}
+  
+  \noindent
+  The first one declares zero for integers and the second the operator for
+  building unions of finite sets (@{text "flat"} having the type 
+  @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"}). 
 
-  \begin{itemize}
-  \item @{text "ABS(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "id"}
-  \item @{text "REP(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"}  =  @{text "id"}
-  \item @{text "ABS(\<sigma>, \<sigma>)"}  =  @{text "id"}
-  \item @{text "REP(\<sigma>, \<sigma>)"}  =  @{text "id"}
-  \item @{text "ABS(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "REP(\<sigma>\<^isub>1,\<tau>\<^isub>1) \<longrightarrow> ABS(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
-  \item @{text "REP(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1) \<longrightarrow> REP(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
-  \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(map \<kappa>) (ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (ABS(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
-  \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(map \<kappa>) (REP(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REP(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
-  \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "Abs_\<kappa>\<^isub>2 \<circ> (map \<kappa>\<^isub>1) (ABS(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (ABS(\<rho>\<^isub>p,\<nu>\<^isub>p)"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
-  \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "(map \<kappa>\<^isub>1) (REP(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REP(\<rho>\<^isub>p,\<nu>\<^isub>p) \<circ> Rep_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
-  \end{itemize}
+  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 \emph{aggregate
+  abstraction} and \emph{representation functions} using the functions @{text "ABS (\<sigma>,
+  \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses we give below. The idea behind
+  these two functions is to simultaneously descend into the raw types @{text \<sigma>} and 
+  quotient types @{text \<tau>}, and generate the appropriate
+  @{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore
+  we generate just the identity whenever the types are equal. On the ``way'' down,
+  however we might have to use map-functions to let @{text Abs} and @{text Rep} act
+  over the appropriate types. In what follows we use the short-hand notation 
+  @{text "ABS (\<sigma>s, \<tau>s)"} to mean @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1)\<dots>ABS (\<sigma>\<^isub>i, \<tau>\<^isub>i)"}; similarly 
+  for @{text REP}.
+  %
+  \begin{center}
+  \hfill
+  \begin{tabular}{rcl}
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ 
+  @{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\\
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\ 
+  @{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{tabular}\hfill\numbered{ABSREP}
+  \end{center}
+  %
+  \noindent
+  In the last two clauses we have that the type @{text "\<alpha>s
+  \<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 among the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by 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{tabular}{rcl}
+  @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a\<^sup>\<alpha>"}\\
+  @{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{tabular}
+  \end{center}
+  %
+  \noindent
+  In this definition we rely on the fact that we can interpret type-variables @{text \<alpha>} as 
+  term variables @{text a}. In the last clause we build an abstraction over all
+  term-variables of the map-function generated by the auxiliary function 
+  @{text "MAP'"}.
+  The need for aggregate map-functions can be seen in cases where 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:
 
-  Apart from the last 2 points the definition is same as the one implemented in
-  in Homeier's HOL package. Adding composition in last two cases is necessary
-  for compositional quotients. We ilustrate the different behaviour of the
-  definition by showing the derived definition of @{term fconcat}:
+  @{text [display, indent=10] "\<lambda>a b. map_prod (map a) b"}
+  
+  \noindent
+  which is essential in order to define the corresponding aggregate 
+  abstraction and representation functions.
+  
+  To see how these definitions pan out in practise, let us return to our
+  example about @{term "concat"} and @{term "fconcat"}, where we have the raw type
+  @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and the quotient type @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>
+  fset"}. Feeding these types into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)
+  the abstraction function
+
+  @{text [display, indent=10] "(map (map id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map id"}
+
+  \noindent
+  In our implementation we further
+  simplify this function by rewriting with 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 simpler abstraction function
+
+  @{text [display, indent=10] "(map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
+
+  \noindent
+  which we can use for defining @{term "fconcat"} as follows
+
+  @{text [display, indent=10] "\<Union> \<equiv> ((map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}
+
+  \noindent
+  Note that by using the operator @{text "\<singlearr>"} and special clauses
+  for function types in \eqref{ABSREP}, we do not have to 
+  distinguish between arguments and results, but can deal with them uniformly.
+  Consequently, all definitions in the quotient package 
+  are of the general form
+
+  @{text [display, indent=10] "c \<equiv> ABS (\<sigma>, \<tau>) t"}
 
-  @{thm fconcat_def[no_vars]}
+  \noindent
+  where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the
+  type of the defined quotient constant @{text "c"}. This data can be easily
+  generated from the declaration given by the user.
+  To increase the confidence in this way of making definitions, we can prove 
+  that the terms involved are all typable.
+
+  \begin{lemma}
+  If @{text "ABS (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"} 
+  and @{text "REP (\<sigma>, \<tau>)"} some representation function @{text "Rep"}, 
+  then @{text "Abs"} is of type @{text "\<sigma> \<Rightarrow> \<tau>"} and @{text "Rep"} of type
+  @{text "\<tau> \<Rightarrow> \<sigma>"}.
+  \end{lemma}
 
-  The aggregate @{term Abs} function takes a finite set of finite sets
-  and applies @{term "map rep_fset"} composed with @{term rep_fset} to
-  its input, obtaining a list of lists, passes the result to @{term concat}
-  obtaining a list and applies @{term abs_fset} obtaining the composed
-  finite set.
+  \begin{proof}
+  By mutual induction and analysing the definitions of @{text "ABS"} and @{text "REP"}. 
+  The cases of equal types 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>)"}). In case of equal type
+  constructors we can observe that a map-function after applying the functions
+  @{text "ABS (\<sigma>s, \<tau>s)"} produces 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"}. This type 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 the
+  @{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>"}, which we just have to compose with
+  @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"} according to the type of @{text "\<circ>"}.\qed
+  \end{proof}
+  
+  \noindent
+  The reader should note that this lemma fails for the abstraction and representation 
+  functions used in Homeier's quotient package.
 *}
 
-subsection {* Respectfulness *}
+section {* Respectfulness and Preservation \label{sec:resp} *}
+
+text {*
+  The main point of the quotient package is to automatically ``lift'' theorems
+  involving constants over the raw type to theorems involving constants over
+  the quotient type. Before we can describe this lifting process, we need to impose 
+  two restrictions in the form of proof obligations that arise during the
+  lifting. The reason is that even if definitions for all raw constants 
+  can be given, \emph{not} all theorems can be lifted to the quotient type. Most 
+  notable is the bound variable function, that is the constant @{text bn}, defined 
+  for raw lambda-terms as follows
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "bn (x) \<equiv> \<emptyset>"}\hspace{4mm}
+  @{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{4mm}
+  @{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}
+  \end{isabelle}
+
+  \noindent
+  We can generate a definition for this constant using @{text ABS} and @{text REP}.
+  But this constant does \emph{not} respect @{text "\<alpha>"}-equivalence and 
+  consequently no theorem involving this constant can be lifted to @{text
+  "\<alpha>"}-equated lambda terms. Homeier formulates the restrictions in terms of
+  the properties of \emph{respectfulness} and \emph{preservation}. We have
+  to slightly extend Homeier's definitions in order to deal with quotient
+  compositions. 
+
+  To formally define what respectfulness is, we have to first define 
+  the notion of \emph{aggregate equivalence relations} using the function @{text REL}:
+
+  \begin{center}
+  \hfill
+  \begin{tabular}{rcl}
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ 
+  @{text "REL (\<sigma>, \<sigma>)"} & $\dn$ & @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
+   \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\ 
+  @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\smallskip\\
+  @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "rel_\<kappa>\<^isub>q (REL (\<sigma>s', \<tau>s))"}\\
+  \end{tabular}\hfill\numbered{REL}
+  \end{center}
+
+  \noindent
+  The @{text "\<sigma>s'"} in the last clause are calculated as in \eqref{ABSREP}:
+  we know that type @{text "\<alpha>s \<kappa>\<^isub>q"} is the quotient of the raw type 
+  @{text "\<rho>s \<kappa>"}. The @{text "\<sigma>s'"} are determined by matching 
+  @{text "\<rho>s \<kappa>"} and @{text "\<sigma>s \<kappa>"}.
+
+  Lets return to the lifting procedure of theorems. Assume we have a theorem
+  that contains the raw constant @{text "c\<^isub>r :: \<sigma>"} and which we want to
+  lift to a theorem where @{text "c\<^isub>r"} is replaced by the corresponding
+  constant @{text "c\<^isub>q :: \<tau>"} defined over a quotient type. In this situation 
+  we generate the following proof obligation
+
+  @{text [display, indent=10] "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
+
+  \noindent
+  Homeier calls these proof obligations \emph{respectfulness
+  theorems}. However, unlike his quotient package, we might have several
+  respectfulness theorems for one constant---he has at most one.
+  The reason is that because of our quotient compositions, the types
+  @{text \<sigma>} and @{text \<tau>} are not completely determined by the type of @{text "c\<^bsub>r\<^esub>"}.
+  And for every instantiation of the types, we might end up with a 
+  corresponding respectfulness theorem.
+
+  Before lifting a theorem, we require the user to discharge
+  respectfulness proof obligations. And the point with @{text bn} is that the respectfulness theorem
+  looks as follows
+
+  @{text [display, indent=10] "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
+
+  \noindent
+  and the user cannot discharge it: because it is not true. To see this,
+  we can just unfold the definition of @{text "\<doublearr>"} \eqref{relfun} 
+  using extensionally to obtain
+
+  @{text [display, indent=10] "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 implies bn(t\<^isub>1) = bn(t\<^isub>2)"}
+ 
+  \noindent
+  In contrast, if we lift a theorem about @{text "append"} to a theorem describing 
+  the union of finite sets, then we need to discharge the proof obligation
+
+  @{text [display, indent=10] "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}
+
+  \noindent
+  To do so, we have to establish
+  
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  if @{text "xs \<approx>\<^bsub>list\<^esub> ys"} and  @{text "us \<approx>\<^bsub>list\<^esub> vs"}
+  then @{text "xs @ us \<approx>\<^bsub>list\<^esub> ys @ vs"}
+  \end{isabelle}
+
+  \noindent
+  which is straightforward given the definition shown in \eqref{listequiv}.
+
+  The second restriction we have to impose arises from
+  non-lifted polymorphic constants, which are instantiated to a
+  type being quotient. For example, take the @{term "cons"}-constructor to 
+  add a pair of natural numbers to a list, whereby teh pair of natural numbers 
+  is to become an integer in te quotient construction. The point is that we 
+  still want to use @{text cons} for
+  adding integers to lists---just with a different type. 
+  To be able to lift such theorems, we need a \emph{preservation property} 
+  for @{text cons}. Assuming we have a polymorphic raw constant 
+  @{text "c\<^isub>r :: \<sigma>"} and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"}, 
+  then a preservation property is as follows
+
+  @{text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies  ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"}
+
+  \noindent
+  where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}.
+  In case of @{text cons} (which has type @{text "\<alpha> \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"}) we have 
+
+  @{text [display, indent=10] "(Rep ---> map Rep ---> map Abs) cons = cons"}
+
+  \noindent
+  under the assumption @{text "Quotient R Abs Rep"}. Interestingly, if we have
+  an instance of @{text cons} where the type variable @{text \<alpha>} is instantiated
+  with @{text "nat \<times> nat"} and we also quotient this type to yield integers,
+  then we need to show the corresponding preservation property.
+
+  %%%@ {thm [display, indent=10] insert_preserve2[no_vars]}
+
+  %Given two quotients, one of which quotients a container, and the
+  %other quotients the type in the container, we can write the
+  %composition of those quotients. To compose two quotient theorems
+  %we compose the relations with relation composition as defined above
+  %and the abstraction and relation functions are the ones of the sub
+  %quotients composed with the usual function composition.
+  %The @ {term "Rep"} and @ {term "Abs"} functions that we obtain agree
+  %with the definition of aggregate Abs/Rep functions and the
+  %relation is the same as the one given by aggregate relations.
+  %This becomes especially interesting
+  %when we compose the quotient with itself, as there is no simple
+  %intermediate step.
+  %
+  %Lets take again the example of @ {term flat}. To be able to lift
+  %theorems that talk about it we provide the composition quotient
+  %theorem which allows quotienting inside the container:
+  %
+  %If @ {term R} is an equivalence relation and @ {term "Quotient R Abs Rep"}
+  %then
+  % 
+  %@ {text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep o rep_fset)"}
+  %%%
+  %%%\noindent
+  %%%this theorem will then instantiate the quotients needed in the
+  %%%injection and cleaning proofs allowing the lifting procedure to
+  %%%proceed in an unchanged way.
+*}
+
+section {* Lifting of Theorems\label{sec:lift} *}
 
 text {*
 
-  A respectfulness lemma for a constant states that the equivalence
-  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
-  the quotient type a respectfulness theorem is required.
-
-  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"}
-  can be stated as:
-
-  @{thm [display] append_rsp[no_vars]}
-
-  \noindent
-  Which after unfolding @{term "op \<Longrightarrow>"} is equivalent to:
-
-  @{thm [display] append_rsp_unfolded[no_vars]}
-
-  An aggregate relation is defined in terms of relation composition,
-  so we define it first:
+  The main benefit of a quotient package is to lift automatically theorems over raw
+  types to theorems over quotient types. We will perform this lifting in
+  three phases, called \emph{regularization},
+  \emph{injection} and \emph{cleaning} according to procedures in Homeier's ML-code.
 
-  \begin{definition}[Composition of Relations]
-  @{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate
-  composition @{thm pred_compI[no_vars]}
-  \end{definition}
-
-  The aggregate relation for an aggregate raw type and quotient type
-  is defined as:
+  The purpose of regularization is to change the quantifiers and abstractions
+  in a ``raw'' theorem to quantifiers over variables that respect the relation
+  (Definition \ref{def:respects} states what respects means). The purpose of injection is to add @{term Rep}
+  and @{term Abs} of appropriate types in front of constants and variables
+  of the raw type so that they can be replaced by the ones that include the
+  quotient type. The purpose of cleaning is to bring the theorem derived in the
+  first two phases into the form the user has specified. Abstractly, our
+  package establishes the following three proof steps:
 
-  \begin{itemize}
-  \item @{text "REL(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "op ="}
-  \item @{text "REL(\<sigma>, \<sigma>)"}  =  @{text "op ="}
-  \item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(rel \<kappa>) (REL(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REL(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
-  \item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "(rel \<kappa>\<^isub>1) (REL(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REL(\<rho>\<^isub>p,\<nu>\<^isub>p) OOO Eqv_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
-
-  \end{itemize}
-
-  Again, the last case is novel, so lets look at the example of
-  respectfullness for @{term concat}. The statement according to
-  the definition above is:
-
-  @{thm [display] concat_rsp[no_vars]}
+  \begin{center}
+  \begin{tabular}{r@ {\hspace{4mm}}l}
+  1.) & @{text "raw_thm \<longrightarrow> reg_thm"}\\
+  2.) & @{text "reg_thm \<longleftrightarrow> inj_thm"}\\
+  3.) & @{text "inj_thm \<longleftrightarrow> quot_thm"}\\
+  \end{tabular}
+  \end{center}
 
   \noindent
-  By unfolding the definition of relation composition and relation map
-  we can see the equivalent statement just using the primitive list
-  equivalence relation:
-
-  @{thm [display] concat_rsp_unfolded[of "a" "a'" "b'" "b", no_vars]}
-
-  The statement reads that, for any lists of lists @{term a} and @{term b}
-  if there exist intermediate lists of lists @{term "a'"} and @{term "b'"}
-  such that each element of @{term a} is in the relation with an appropriate
-  element of @{term a'}, @{term a'} is in relation with @{term b'} and each
-  element of @{term b'} is in relation with the appropriate element of
-  @{term b}.
-
-*}
-
-subsection {* Preservation *}
-
-text {*
-  To be able to lift theorems that talk about constants that are not
-  lifted but whose type changes when lifting is performed additionally
-  preservation theorems are needed.
-
-  To lift theorems that talk about insertion in lists of lifted types
-  we need to know that for any quotient type with the abstraction and
-  representation functions @{text "Abs"} and @{text Rep} we have:
-
-  @{thm [display] (concl) cons_prs[no_vars]}
-
-  This is not enough to lift theorems that talk about quotient compositions.
-  For some constants (for example empty list) it is possible to show a
-  general compositional theorem, but for @{term "op #"} it is necessary
-  to show that it respects the particular quotient type:
-
-  @{thm [display] insert_preserve2[no_vars]}
-*}
-
-subsection {* Composition of Quotient theorems *}
+  which means the raw theorem implies the quotient theorem.
+  In contrast to other quotient packages, our package requires
+  the \emph{term} of the @{text "quot_thm"} to be given by the user.\footnote{Though we
+  also provide a fully automated mode, where the @{text "quot_thm"} is guessed
+  from the form of @{text "raw_thm"}.} As a result, it is possible that a user can lift only some
+  occurrences of a raw type, but not others. 
 
-text {*
-  Given two quotients, one of which quotients a container, and the
-  other quotients the type in the container, we can write the
-  composition of those quotients. To compose two quotient theorems
-  we compose the relations with relation composition as defined above
-  and the abstraction and relation functions are the ones of the sub
-  quotients composed with the usual function composition.
-  The @{term "Rep"} and @{term "Abs"} functions that we obtain agree
-  with the definition of aggregate Abs/Rep functions and the
-  relation is the same as the one given by aggregate relations.
-  This becomes especially interesting
-  when we compose the quotient with itself, as there is no simple
-  intermediate step.
-
-  Lets take again the example of @{term concat}. To be able to lift
-  theorems that talk about it we provide the composition quotient
-  theorems, which then lets us perform the lifting procedure in an
-  unchanged way:
-
-  @{thm [display] quotient_compose_list[no_vars]}
-*}
-
-
-section {* Lifting Theorems *}
+  The second and third proof step will always succeed if the appropriate
+  respectfulness and preservation theorems are given. In contrast, the first
+  proof step can fail: a theorem given by the user does not always
+  imply a regularized version and a stronger one needs to be proved. This
+  is outside of the scope where the quotient package can help. An example
+  for this kind of failure is the simple statement for integers @{text "0 \<noteq> 1"}.
+  One might hope that it can be proved by lifting @{text "(0, 0) \<noteq> (1, 0)"},  
+  but the raw theorem only shows that particular element in the
+  equivalence classes are not equal. A more general statement stipulating that
+  the equivalence classes are not equal is necessary, and then leads to the
+  theorem  @{text "0 \<noteq> 1"}.
 
-text {*
-  The core of the quotient package takes an original theorem that
-  talks about the raw types, and the statement of the theorem that
-  it is supposed to produce. This is different from other existing
-  quotient packages, where only the raw theorems were necessary.
-  We notice that in some cases only some occurrences of the raw
-  types need to be lifted. This is for example the case in the
-  new Nominal package, where a raw datatype that talks about
-  pairs of natural numbers or strings (being lists of characters)
-  should not be changed to a quotient datatype with constructors
-  taking integers or finite sets of characters. To simplify the
-  use of the quotient package we additionally provide an automated
-  statement translation mechanism that replaces occurrences of
-  types that match given quotients by appropriate lifted types.
+  In the following we will first define the statement of the
+  regularized theorem based on @{text "raw_thm"} and
+  @{text "quot_thm"}. Then we define the statement of the injected theorem, based
+  on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps,
+  which can all be performed independently from each other.
 
-  Lifting the theorems is performed in three steps. In the following
-  we call these steps \emph{regularization}, \emph{injection} and
-  \emph{cleaning} following the names used in Homeier's HOL
-  implementation.
-
-  We first define the statement of the regularized theorem based
-  on the original theorem and the goal theorem. Then we define
-  the statement of the injected theorem, based on the regularized
-  theorem and the goal. We then show the 3 proofs, as all three
-  can be performed independently from each other.
-
-*}
-
-subsection {* Regularization and Injection statements *}
-
-text {*
-
-  We first define the function @{text REG}, which takes the statements
-  of the raw theorem and the lifted theorem (both as terms) and
-  returns the statement of the regularized version. The intuition
+  We first define the function @{text REG}. The intuition
   behind this function is that it replaces quantifiers and
   abstractions involving raw types by bounded ones, and equalities
   involving raw types are replaced by appropriate aggregate
-  relations. It is defined as follows:
+  equivalence relations. It is defined as follows:
+
+  \begin{center}
+  \begin{longtable}{rcl}
+  \multicolumn{3}{@ {}l}{abstractions:}\smallskip\\
+  @{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} & $\dn$ & 
+  $\begin{cases}
+  @{text "\<lambda>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+  @{text "\<lambda>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
+  \end{cases}$\smallskip\\
+  \\
+  \multicolumn{3}{@ {}l}{universal quantifiers:}\\
+  @{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} & $\dn$ & 
+  $\begin{cases}
+  @{text "\<forall>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+  @{text "\<forall>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
+  \end{cases}$\smallskip\\
+  \multicolumn{3}{@ {}l}{equality:}\smallskip\\
+  %% REL of two equal types is the equality so we do not need a separate case
+  @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>)"}\\\smallskip\\
+  \multicolumn{3}{@ {}l}{applications, variables and constants:}\\
+  @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} & $\dn$ & @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
+  @{text "REG (x\<^isub>1, x\<^isub>2)"} & $\dn$ & @{text "x\<^isub>1"}\\
+  @{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\[-5mm]
+  \end{longtable}
+  \end{center}
+  %
+  \noindent
+  In the above definition we omitted the cases for existential quantifiers
+  and unique existential quantifiers, as they are very similar to the cases
+  for the universal quantifier. For the third and fourt clause, note that 
+  @{text "\<forall>x. P"} is defined as @{text "\<forall> (\<lambda>x. P)"}.
+
+  Next we define the function @{text INJ} which takes as argument
+  @{text "reg_thm"} and @{text "quot_thm"} (both as
+  terms) and returns @{text "inj_thm"}:
+
+  \begin{center}
+  \begin{tabular}{rcl}
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions:}\\
+  @{text "INJ (\<lambda>x. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$ & 
+  $\begin{cases}
+  @{text "\<lambda>x. INJ (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+  @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x. INJ (t, s)))"}
+  \end{cases}$\\
+  @{text "INJ (\<lambda>x \<in> R. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$ 
+  & @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x \<in> R. INJ (t, s)))"}\smallskip\\
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{universal quantifiers:}\\
+  @{text "INJ (\<forall> t, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s)"}\\
+  @{text "INJ (\<forall> t \<in> R, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s) \<in> R"}\smallskip\\
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables and constants:}\smallskip\\
+  @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) "} & $\dn$ & @{text " INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}\\
+  @{text "INJ (x\<^isub>1\<^sup>\<sigma>, x\<^isub>2\<^sup>\<tau>) "} & $\dn$ & 
+  $\begin{cases}
+  @{text "x\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+  @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) x\<^isub>1)"}\\
+  \end{cases}$\\
+  @{text "INJ (c\<^isub>1\<^sup>\<sigma>, c\<^isub>2\<^sup>\<tau>) "} & $\dn$ & 
+  $\begin{cases}
+  @{text "c\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+  @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) c\<^isub>1)"}\\
+  \end{cases}$\\
+  \end{tabular}
+  \end{center}
+
+  \noindent 
+  where again the cases for existential quantifiers and unique existential
+  quantifiers have been omitted.
+
+  In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always 
+  start with an implication. Isabelle provides \emph{mono} rules that can split up 
+  the implications into simpler implication subgoals. This succeeds for every
+  monotone connective, except in places where the function @{text REG} inserted,
+  for instance, a quantifier by a bounded quantifier. In this case we have 
+  rules of the form
+
+  @{text [display, indent=10] "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}
+
+  \noindent
+  They decompose a bounded quantifier on the right-hand side. We can decompose a
+  bounded quantifier anywhere if R is an equivalence relation or
+  if it is a relation over function types with the range being an equivalence
+  relation. If @{text R} is an equivalence relation we can prove that
+
+  @{text [display, indent=10] "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}    
+
+  \noindent
+  And when @{term R\<^isub>2} is an equivalence relation and we can prove
+
+  @{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
+
+  \noindent
+  The last theorem is new in comparison with Homeier's package. There the
+  injection procedure would be used to prove such goals, and 
+  the assumption about the equivalence relation would be used. We use the above theorem directly,
+  because this allows us to completely separate the first and the second
+  proof step into two independent ``units''.
+
+  The second proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"},  starts with an equality. 
+  The proof again follows the structure of the
+  two underlying terms, and is defined for a goal being a relation between these two terms.
 
   \begin{itemize}
-  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"}
-  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
-  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"}
-  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
-  \item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"}
-  \item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"}
-  \item @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}
-  \item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"}
-  \item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"}
-  \end{itemize}
-
-  In the above definition we ommited the cases for existential quantifiers
-  and unique existential quantifiers, as they are very similar to the cases
-  for the universal quantifier.
+  \item For two constants an appropriate constant respectfulness lemma is applied.
+  \item For two variables, we use the assumptions proved in the regularization step.
+  \item For two abstractions, we @{text "\<eta>"}-expand and @{text "\<beta>"}-reduce them.
+  \item For two applications, we check that the right-hand side is an application of
+    @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"}. If yes then we
+    can apply the theorem:
 
-  Next we define the function @{text INJ} which takes the statement of
-  the regularized theorems and the statement of the lifted theorem both as
-  terms and returns the statment of the injected theorem:
+    @{term [display, indent=10] "R x y \<longrightarrow> R x (Rep (Abs y))"}
 
-  \begin{itemize}
-  \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"}
-  \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"}
-  \item @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"}
-  \item @{text "INJ (\<forall> t, \<forall> s) = \<forall> (INJ (t, s)"}
-  \item @{text "INJ (\<forall> t \<in> R, \<forall> s) = \<forall> (INJ (t, s) \<in> R"}
-  \item @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}
-  \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) = v\<^isub>1"}
-  \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"}
-  \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) = c\<^isub>1"}
-  \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"}
+    Otherwise we introduce an appropriate relation between the subterms
+    and continue with two subgoals using the lemma:
+
+    @{text [display, indent=10] "(R\<^isub>1 \<doublearr> R\<^isub>2) f g \<longrightarrow> R\<^isub>1 x y \<longrightarrow> R\<^isub>2 (f x) (g y)"}
   \end{itemize}
 
-  For existential quantifiers and unique existential quantifiers it is
-  defined similarily to the universal one.
-
-*}
-
-subsection {* Proof procedure *}
-
-(* In the below the type-guiding 'QuotTrue' assumption is removed; since we
-   present in a paper a version with typed-variables it is not necessary *)
-
-text {*
-
-  With the above definitions of @{text "REG"} and @{text "INJ"} we can show
-  how the proof is performed. The first step is always the application of
-  of the following lemma:
-
-  @{term "[|A; A --> B; B = C; C = D|] ==> D"}
-
-  With @{text A} instantiated to the original raw theorem, 
-       @{text B} instantiated to @{text "REG(A)"},
-       @{text C} instantiated to @{text "INJ(REG(A))"},
-   and @{text D} instantiated to the statement of the lifted theorem.
-  The first assumption can be immediately discharged using the original
-  theorem and the three left subgoals are exactly the subgoals of regularization,
-  injection and cleaning. The three can be proved independently by the
-  framework and in case there are non-solved subgoals they can be left
-  to the user.
-
-  The injection and cleaning subgoals are always solved if the appropriate
-  respectfulness and preservation theorems are given. It is not the case
-  with regularization; sometimes a theorem given by the user does not
-  imply a regularized version and a stronger one needs to be proved. This
-  is outside of the scope of the quotient package, so the user is then left
-  with such obligations. As an example lets see the simplest possible
-  non-liftable theorem for integers: When we want to prove @{term "0 \<noteq> 1"}
-  on integers the fact that @{term "\<not> (0, 0) = (1, 0)"} is not enough. It
-  only shows that particular items in the equivalence classes are not equal,
-  a more general statement saying that the classes are not equal is necessary.
-*}
-
-subsection {* Proving Regularization *}
-
-text {*
-
-  Isabelle provides a set of \emph{mono} rules, that are used to split implications
-  of similar statements into simpler implication subgoals. These are enchanced
-  with special quotient theorem in the regularization goal. Below we only show
-  the versions for the universal quantifier. For the existential quantifier
-  and abstraction they are analoguous with some symmetry.
-
-  First, bounded universal quantifiers can be removed on the right:
-
-  @{thm [display] ball_reg_right[no_vars]}
-
-  They can be removed anywhere if the relation is an equivalence relation:
-
-  @{thm [display] ball_reg_eqv[no_vars]}
-
-  And finally it can be removed anywhere if @{term R2} is an equivalence relation, then:
-  \[
-  @{thm (rhs) ball_reg_eqv_range[no_vars]} = @{thm (lhs) ball_reg_eqv_range[no_vars]}
-  \]
+  We defined the theorem @{text "inj_thm"} in such a way that
+  establishing the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be
+  achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient
+  definitions. Then for all lifted constants, their definitions
+  are used to fold the @{term Rep} with the raw constant. Next for
+  all abstractions and quantifiers the lambda and
+  quantifier preservation theorems are used to replace the
+  variables that include raw types with respects by quantifiers
+  over variables that include quotient types. We show here only
+  the lambda preservation theorem. Given
+  @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}, we have:
 
-  The last theorem is new in comparison with Homeier's package; it allows separating
-  regularization from injection.
-
-*}
-
-(*
-  @{thm (rhs) bex_reg_eqv_range[no_vars]} = @{thm (lhs) bex_reg_eqv_range[no_vars]}
-  @{thm [display] bex_reg_left[no_vars]}
-  @{thm [display] bex1_bexeq_reg[no_vars]}
-  @{thm [display] bex_reg_eqv[no_vars]}
-  @{thm [display] babs_reg_eqv[no_vars]}
-  @{thm [display] babs_simp[no_vars]}
-*)
-
-subsection {* Injection *}
+    @{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
 
-text {*
-  The injection proof starts with an equality between the regularized theorem
-  and the injected version. The proof again follows by the structure of the
-  two term, and is defined for a goal being a relation between the two terms.
-
-  \begin{itemize}
-  \item For two constants, an appropriate constant respectfullness assumption is used.
-  \item For two variables, the regularization assumptions state that they are related.
-  \item For two abstractions, they are eta-expanded and beta-reduced.
-  \end{itemize}
-
-  Otherwise the two terms are applications. There are two cases: If there is a REP/ABS
-  in the injected theorem we can use the theorem:
-
-  @{thm [display] rep_abs_rsp[no_vars]}
+  \noindent
+  Next, relations over lifted types are folded to equalities.
+  For this the following theorem has been shown in Homeier~\cite{Homeier05}:
 
-  and continue the proof.
-
-  Otherwise we introduce an appropriate relation between the subterms and continue with
-  two subgoals using the lemma:
-
-  @{thm [display] apply_rsp[no_vars]}
-
-*}
-
-subsection {* Cleaning *}
-
-text {*
-  The @{text REG} and @{text INJ} functions have been defined in such a way
-  that establishing the goal theorem now consists only on rewriting the
-  injected theorem with the preservation theorems.
+    @{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]}
 
-  \begin{itemize}
-  \item First for lifted constants, their definitions are the preservation rules for
-    them.
-  \item For lambda abstractions lambda preservation establishes
-    the equality between the injected theorem and the goal. This allows both
-    abstraction and quantification over lifted types.
-    @{thm [display] lambda_prs[no_vars]}
-  \item Relations over lifted types are folded with:
-    @{thm [display] Quotient_rel_rep[no_vars]}
-  \item User given preservation theorems, that allow using higher level operations
-    and containers of types being lifted. An example may be
-    @{thm [display] map_prs(1)[no_vars]}
-  \end{itemize}
+  \noindent
+  Finally, we rewrite with the preservation theorems. This will result
+  in two equal terms that can be solved by reflexivity.
+  *}
 
- Preservation of relations and user given constant preservation lemmas *}
-
-section {* Examples *}
+section {* Examples \label{sec:examples} *}
 
 (* Mention why equivalence *)
 
 text {*
 
-  A user of our quotient package first needs to define an equivalence relation:
+  In this section we will show, a complete interaction with the quotient package
+  for defining the type of integers by quotienting pairs of natural numbers and
+  lifting theorems to integers. Our quotient package is fully compatible with
+  Isabelle type classes, but for clarity we will not use them in this example.
+  In a larger formalization of integers using the type class mechanism would
+  provide many algebraic properties ``for free''.
 
-  @{text "fun \<approx> where (x, y) \<approx> (u, v) = (x + v = u + y)"}
-
-  Then the user defines a quotient type:
+  A user of our quotient package first needs to define a relation on
+  the raw type, by which the quotienting will be performed. We give
+  the same integer relation as the one presented in \eqref{natpairequiv}:
 
-  @{text "quotient_type int = (nat \<times> nat) / \<approx>"}
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \begin{tabular}{@ {}l}
+  \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"}\\
+  \isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"}
+  \end{tabular}
+  \end{isabelle}
 
-  Which leaves a proof obligation that the relation is an equivalence relation,
-  that can be solved with the automatic tactic with two definitions.
+  \noindent
+  Next the quotient type is defined. This generates a proof obligation that the
+  relation is an equivalence relation, which is solved automatically using the
+  definition and extensionality:
 
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \begin{tabular}{@ {}l}
+  \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"}\\
+  \hspace{5mm}@{text "by (auto simp add: equivp_def expand_fun_eq)"}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
   The user can then specify the constants on the quotient type:
 
-  @{text "quotient_definition 0 \<Colon> int is (0\<Colon>nat, 0\<Colon>nat)"}
-  @{text "fun plus_raw where plus_raw (x, y) (u, v) = (x + u, y + v)"}
-  @{text "quotient_definition (op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int) is plus_raw"}
-
-  Lets first take a simple theorem about addition on the raw level:
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \begin{tabular}{@ {}l}
+  \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\[3mm]
+  \isacommand{fun}~~@{text "add_pair"}~~\isacommand{where}~~%
+  @{text "add_pair (m, n) (p, q) \<equiv> (m + p :: nat, n + q :: nat)"}\\
+  \isacommand{quotient\_definition}~~@{text "+ :: int \<Rightarrow> int \<Rightarrow> int"}~~%
+  \isacommand{is}~~@{text "add_pair"}\\
+  \end{tabular}
+  \end{isabelle}
 
-  @{text "lemma plus_zero_raw: plus_raw (0, 0) i \<approx> i"}
+  \noindent
+  The following theorem about addition on the raw level can be proved.
 
-  When the user tries to lift a theorem about integer addition, the respectfulness
-  proof obligation is left, so let us prove it first:
-  
-  @{text "lemma (op \<approx> \<Longrightarrow> op \<approx> \<Longrightarrow> op \<approx>) plus_raw plus_raw"}
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \isacommand{lemma}~~@{text "add_pair_zero: int_rel (add_pair (0, 0) x) x"}
+  \end{isabelle}
+
+  \noindent
+  If the user attempts to lift this theorem, all proof obligations are 
+  automatically discharged, except the respectfulness
+  proof for @{text "add_pair"}:
 
-  Can be proved automatically by the system just by unfolding the definition
-  of @{term "op \<Longrightarrow>"}.
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \begin{tabular}{@ {}l}
+  \isacommand{lemma}~~@{text "[quot_respect]:"}\\ 
+  @{text "(int_rel \<doublearr> int_rel \<doublearr> int_rel) add_pair add_pair"}
+  \end{tabular}
+  \end{isabelle}
 
-  Now the user can either prove a lifted lemma explicitely:
+  \noindent
+  This can be discharged automatically by Isabelle when telling it to unfold the definition
+  of @{text "\<doublearr>"}.
+  After this, the user can prove the lifted lemma explicitly:
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting add_pair_zero"}
+  \end{isabelle}
 
-  @{text "lemma 0 + i = i by lifting plus_zero_raw"}
+  \noindent
+  or by the completely automated mode by stating:
 
-  Or in this simple case use the automated translation mechanism:
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \isacommand{thm}~~@{text "add_pair_zero[quot_lifted]"}
+  \end{isabelle}
 
-  @{text "thm plus_zero_raw[quot_lifted]"}
+  \noindent
+  Both methods give the same result, namely
 
-  obtaining the same result.
+  @{text [display, indent=10] "0 + x = x"}
+
+  \noindent
+  Although seemingly simple, arriving at this result without the help of a quotient
+  package requires a substantial reasoning effort.
 *}
 
-section {* Related Work *}
+section {* Conclusion and Related Work\label{sec:conc}*}
 
 text {*
-  \begin{itemize}
 
-  \item Peter Homeier's package~\cite{Homeier05} (and related work from there)
-  \item John Harrison's one~\cite{harrison-thesis} is the first one to lift theorems
-    but only first order.
-
-  \item PVS~\cite{PVS:Interpretations}
-  \item MetaPRL~\cite{Nogin02}
-  \item Manually defined quotients in Isabelle/HOL Library (Markus's Quotient\_Type,
-    Dixon's FSet, \ldots)
+  The code of the quotient package and the examples described here are
+  already included in the
+  standard distribution of Isabelle.\footnote{Available from
+  \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is
+  heavily used in the new version of Nominal Isabelle, which provides a convenient reasoning
+  infrastructure for programming language calculi involving general binders.  
+  To achieve this, it builds types representing @{text \<alpha>}-equivalent terms.
+  Earlier
+  versions of Nominal Isabelle have been used successfully in formalisations
+  of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08},
+  Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for
+  concurrency \cite{BengtsonParow09} and a strong normalisation result for
+  cut-elimination in classical logic \cite{UrbanZhu08}.
 
-  \item Oscar Slotosch defines quotient-type automatically but no
-    lifting~\cite{Slotosch97}.
-
-  \item PER. And how to avoid it.
+  There is a wide range of existing of literature for dealing with
+  quotients in theorem provers.
+  Slotosch~\cite{Slotosch97} implemented a mechanism that automatically
+  defines quotient types for Isabelle/HOL. But he did not include theorem lifting.
+  Harrison's quotient package~\cite{harrison-thesis} is the first one that is
+  able to automatically lift theorems, however only first-order theorems (that is theorems
+  where abstractions, quantifiers and variables do not involve functions that
+  include the quotient type). 
+  There is also some work on quotient types in
+  non-HOL based systems and logical frameworks, including theory interpretations
+  in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, 
+  and setoids in Coq \cite{ChicliPS02}.
+  Paulson showed a construction of quotients that does not require the
+  Hilbert Choice operator, but also only first-order theorems can be lifted~\cite{Paulson06}.
+  The most related work to our package is the package for HOL4 by Homeier~\cite{Homeier05}.
+  He introduced most of the abstract notions about quotients and also deals with the
+  lifting of higher-order theorems. However, he cannot deal with quotient compositions (needed
+  for lifting theorems about @{text flat}). Also, a number of his definitions, like @{text ABS},
+  @{text REP} and @{text INJ} etc only exist in \cite{Homeier05} as ML-code, not included
+  in the paper. 
 
-  \item Necessity of Hilbert Choice op and Larry's quotients~\cite{Paulson06}
+  One advantage of our package is that it is modular---in the sense that every step
+  in the quotient construction can be done independently (see the criticism of Paulson
+  about other quotient packages). This modularity is essential in the context of
+  Isabelle, which supports type-classes and locales.
 
-  \item Setoids in Coq and \cite{ChicliPS02}
+  Another feature of our quotient package is that when lifting theorems, teh user can
+  precisely specify what the lifted theorem should look like. This feature is
+  necessary, for example, when lifting an induction principle for two lists.
+  This principle has as the conclusion a predicate of the form @{text "P xs ys"},
+  and we can precisely specify whether we want to quotient @{text "xs"} or @{text "ys"},
+  or both. We found this feature very useful in the new version of Nominal 
+  Isabelle, where such a choice is required to generate a resoning infrastructure
+  for alpha-equated terms. 
+%%
+%% give an example for this
+%%
+  \medskip
 
-  \end{itemize}
+  \noindent
+  {\bf Acknowledgements:} We would like to thank Peter Homeier for the many
+  discussions about his HOL4 quotient package and explaining to us
+  some of its finer points in the implementation. Without his patient
+  help, this work would have been impossible.
+
 *}
 
-section {* Conclusion *}
+
 
 (*<*)
 end