(* How to change the notation for \<lbrakk> \<rbrakk> meta-level implications? *)

(*<*)

theory Paper

imports "Quotient"

        "LaTeXsugar"

        "../Nominal/FSet"

begin

notation (latex output)

  rel_conj ("_ OOO _" [53, 53] 52) and

  "op -->" (infix "\<rightarrow>" 100) and

  "==>" (infix "\<Rightarrow>" 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>") 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 =

      Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)

  in

    case concl of (_ $ l $ r) => proj (l, r)

    | _ => 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 {* 

   \begin{flushright}

  {\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}

  \noindent

  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

  \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_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}

  \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.

  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

  \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

  prove formally, for example, 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. 

  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}

  \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 starting point is an existing type, to which we 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 elements 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

  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_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_int (add_pair (Rep_int n) (Rep_int m))"}

  \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, indent=10] concat.simps(1) concat.simps(2)[no_vars]}

  \noindent

  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 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 case in case

  of @{text "\<Union>"} we obtain the incorrect definition

  @{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

  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 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 needs to be

  done 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 respectfullness

  and preservation.\ldots

*}

section {* Preliminaries and General Quotient\label{sec:prelims} *}

text {*

  In this section we present the definitions of a quotient that follow

  closely those given by Homeier.

  \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{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]}

  \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}

  Higher Order Logic 

  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}

  {\it Say more about containers / maping functions }

  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.

  {\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 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 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"}

  \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 earlier in \eqref{natpairequiv} and

  \eqref{listequiv}, respectively (the proofs about being equivalence

  relations is omitted).  Given this data, we declare internally 

  the quotient types 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 restriction 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 provide us with the following

  abstraction and representation functions having the type

  \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 

  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

  \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

  \begin{property}

  @{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}

  \end{property}

  \noindent

  holds  for every quotient type defined

  as above (for the proof see \cite{Homeier05}).

  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 visible 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 are 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. 

  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 recursively 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. All clauses

  are as follows:

  \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

  where in the last two clauses we have that the quotient 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 inside map-function generated by the auxiliary function 

  @{text "MAP'"}.

  The need of 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:

  @{text [display, indent=10] "\<lambda>a b. map_prod (map a) b"}

  \noindent

  which we need to define the aggregate abstraction and representation functions.

  To see how these definitions pan out in practise, let us return to our