52   \end{flushright}\smallskip

    52   \end{flushright}

    67   @{text [display, indent=10] "(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"}

    67   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

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

    69   \end{isabelle}

    80   @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}

    82   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

    83   @{text "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}\hfill\numbered{listequiv}

    84   \end{isabelle}

   148   type}, over which an equivalence relation given by the user is

   152   type}, over which an equivalence relation given by the user is defined. With

   149   defined. With this input the package introduces a new type, to which we

   153   this input the package introduces a new type, to which we refer as the

   150   refer as the \emph{quotient type}. This type comes with an

   154   \emph{quotient type}. This type comes with an \emph{abstraction} and a

   151   \emph{abstraction} and a \emph{representation} function, written @{text Abs}

   155   \emph{representation} function, written @{text Abs} and @{text

   152   and @{text Rep}.\footnote{Actually they need to be derived from slightly

   156   Rep}.\footnote{Actually slightly more basic functions are given; the @{text Abs}

   153   more basic functions. We will show the details later. } These functions

   157   and @{text Rep} need to be derived from them. We will show the details

   154   relate elements in the existing type to ones in the new type and vice versa;

   158   later. } These functions relate elements in the existing type to ones in the

   155   they can be uniquely identified by their type. For example for the integer

   159   new type and vice versa; they can be uniquely identified by their type. For

   156   quotient construction the types of @{text Abs} and @{text Rep} are

   160   example for the integer quotient construction the types of @{text Abs} and

   161   @{text Rep} are

   228   of \emph{aggregate relation}, \emph{respectfulness} and \emph{preservation}

   233   of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}

   231   We will also address the criticism by Paulson \cite{Paulson06} cited at the

   236   We are also able to address the criticism by Paulson \cite{Paulson06} cited

   232   beginning of this section about having to collect theorems that are lifted from the raw

   237   at the beginning of this section about having to collect theorems that are

   233   level to the quotient level. Our quotient package is the first one that is modular so that it

   238   lifted from the raw level to the quotient level. Our quotient package is the

   234   allows to lift single theorems separately. This has the advantage for the

   239   first one that is modular so that it allows to lift single theorems

   235   user to develop a formal theory interactively an a natural progression. A

   240   separately. This has the advantage for the user to develop a formal theory

   236   pleasing result of the modularity is also that we are able to clearly

   241   interactively an a natural progression. A pleasing result of the modularity

   237   specify what needs to be done in the lifting process (this was only hinted at in

   242   is also that we are able to clearly specify what needs to be done in the

   238   \cite{Homeier05} and implemented as a ``rough recipe'' in ML-code).

   243   lifting process (this was only hinted at in \cite{Homeier05} and implemented

   239  

   244   as a ``rough recipe'' in ML-code).

   240   The paper is organised as follows \ldots

   245 

   241 *}

   246   The paper is organised as follows: Section \ref{sec:prelims} presents briefly

   242 

   247   some necessary preliminaries; Section \ref{sec:type} presents the definitions 

   248   of quotient types and shows how definitions can be made over quotient types. \ldots

   249 *}

   299 *}

   304   Such maps for most common types (list, pair, sum,

   300 

   305   option, \ldots) are described in Homeier, and we assume that @{text "map"}

   301 section {* Quotient Types and Lifting of Definitions *}

   306   is the function that returns a map for a given type.

   307 

   308 *}

   309 

   310 section {* Quotient Types and Quotient Definitions\label{sec:type} *}

   315   and a proof that @{text "R"} is indeed an equivalence relation.

   324   and a proof that @{text "R"} is indeed an equivalence relation. Two concrete

   316   Given this data, we can internally declare the quotient type as

   325   examples are

   326 

   327   

   328   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   329   \begin{tabular}{@ {}l}

   330   \isacommand{quotient\_type}~~@{text "int = nat \<times> nat / \<approx>\<^bsub>nat \<times> nat\<^esub>"}\\

   331   \isacommand{quotient\_type}~~@{text "\<alpha> fset = \<alpha> list / \<approx>\<^bsub>list\<^esub>"}

   332   \end{tabular}

   333   \end{isabelle}

   334 

   335   \noindent

   336   which introduce the type of integers and of finite sets using the

   337   equivalence relations @{text "\<approx>\<^bsub>nat \<times> nat\<^esub>"} and @{text

   338   "\<approx>\<^bsub>list\<^esub>"} defined earlier in \eqref{natpairequiv} and

   339   \eqref{listequiv}, respectively.  Given this data, we declare internally 

   340   the quotient types as

   323   being the (non-empty) set of equivalence classes of @{text "R"}. The

   347   where the right hand side is the (non-empty) set of equivalence classes of

   324   restriction in this declaration is that the type variables in the raw type

   348   @{text "R"}. The restriction in this declaration is that the type variables

   325   @{text "\<sigma>"} must be included in the type variables @{text "\<alpha>s"} declared for

   349   in the raw type @{text "\<sigma>"} must be included in the type variables @{text

   326   @{text "\<kappa>\<^isub>q"}. HOL will provide us with abstraction and

   350   "\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will provide us with

   327   representation functions having the type

   351   abstraction and representation functions having the type

   344   definition of @{text "Rep_\<kappa>\<^isub>q"}. These derived notions relate the quotient type

   368   definition of @{text "Rep_\<kappa>\<^isub>q"}. These derived notions relate the

   345   and the raw type directly, as can be seen from their type, namely @{text "\<sigma>

   369   quotient type and the raw type directly, as can be seen from their type,

   346   \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"}, respectively.  Given that

   370   namely @{text "\<sigma> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"},

   347   @{text "R"} is an equivalence relation, the following property

   371   respectively.  Given that @{text "R"} is an equivalence relation, the

   372   following property

   373 

   354   The next step is to lift definitions over the raw type to definitions over the

   380   The next step is to introduce new definitions involving the quotient type,

   355   quotient type. For this we provide the declaration

   381   which need to be defined in terms of concepts of the raw type (remember this 

   356 

   382   is the only way how toe be able to extend HOL with new definitions). For the

   357   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   383   user visible is the declaration

   358   \isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~\isacommand{is}~@{text "c' :: \<sigma>"}

   384 

   359   \end{isabelle}

   385   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   360 

   386   \isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~~\isacommand{is}~~@{text "t :: \<sigma>"}

   361   To define a constant on the lifted type, an aggregate abstraction

   387   \end{isabelle}

   362   function is applied to the raw constant. Below we describe the operation

   388 

   363   that generates

   389   \noindent

   364   an aggregate @{term "Abs"} or @{term "Rep"} function given the

   390   where @{text t} is the definiens (its type @{text \<sigma>} can always be inferred)

   365   compound raw type and the compound quotient type.

   391   and @{text "c"} is the name of definiendum, whose type @{text "\<tau>"} needs to be

   366   This operation will also be used in translations of theorem statements

   392   given explicitly (the point is that @{text "\<tau>"} and @{text "\<sigma>"} can only differ 

   367   and in the lifting procedure.

   393   in places where a quotient and raw type are involved). Two examples are

   368 

   394 

   369   The operation is additionally able to descend into types for which

   395   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   370   maps are known. Such maps for most common types (list, pair, sum,

   396   \begin{tabular}{@ {}l}

   371   option, \ldots) are described in Homeier, and we assume that @{text "map"}

   397   \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0::nat, 0::nat)"}\\

   372   is the function that returns a map for a given type. Then REP/ABS is defined

   398   \isacommand{quotient\_definition}~~@{text "\<Union> :: (\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}~~%

   373   as follows:

   399   \isacommand{is}~~@{text "flat"} 

   374 

   400   \end{tabular}

   375   {\it the first argument is the raw type and the second argument the quotient type}

   401   \end{isabelle}

   376   %

   402   

   403   \noindent

   404   The first one declares zero for integers and the second the operator for

   405   building unions of finite sets. The problem for us is that from such

   406   declarations we need to derive proper definitions using the @{text "Abs"}

   407   and @{text "Rep"} functions for the quotient types involved. The data we

   408   rely on is the given quotient type @{text "\<tau>"} and the raw type @{text "\<sigma>"}.

   409   They allow us to define aggregate abstraction and representation functions

   410   using the functions @{text "ABS (\<sigma>, \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose 

   411   clauses are given below. The idea behind them is to recursively descend into 

   412   both types and generate the appropriate @{text "Abs"} and @{text "Rep"} 

   413   in places where the types differ. Therefore we returning just the identity

   414   whenever the types are equal.

   415 

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

   429   @{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"}

   395   where in the last two clauses we have that the quotient type @{text "\<alpha>s \<kappa>\<^isub>q"} is a quotient of

   434   where in the last two clauses we have that the quotient type @{text "\<alpha>s

   396   the raw type @{text "\<rho>s \<kappa>"} (for example @{text "\<alpha> fset"} and @{text "\<alpha> list"}). 

   435   \<kappa>\<^isub>q"} is a quotient of the raw type @{text "\<rho>s \<kappa>"} (for example

   397   The quotient construction ensures that the type variables in @{text "\<rho>s"} 

   436   @{text "int"} and @{text "nat \<times> nat"}, or @{text "\<alpha> fset"} and @{text "\<alpha>

   398   must be amongst the @{text "\<alpha>s"}. Now the @{text "\<sigma>s'"} are given by the matchers 

   437   list"}). The quotient construction ensures that the type variables in @{text

   399   for the @{text "\<alpha>s"} 

   438   "\<rho>s"} must be amongst the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the

   400   when matching  @{text "\<sigma>s \<kappa>\<^isub>q"} against @{text "\<alpha>s \<kappa>\<^isub>q"}; similarly the @{text "\<tau>s'"} are given by the 

   439   matchers for the @{text "\<alpha>s"} when matching @{text "\<sigma>s \<kappa>\<^isub>q"} against

   401   same type-variables when matching @{text "\<tau>s \<kappa>"} against @{text "\<rho>s \<kappa>"}.

   440   @{text "\<alpha>s \<kappa>\<^isub>q"}; similarly the @{text "\<tau>s'"} are given by the same

   402   The function @{text "MAP"} calculates an \emph{aggregate map-function} for a type 

   441   type-variables when matching @{text "\<tau>s \<kappa>"} against @{text "\<rho>s \<kappa>"}.  The

   403   as follows:

   442   function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw

   404 

   443   type as follows:

   444   %

   406   \begin{tabular}{rcl}

   446   \begin{longtable}{rcl}

   407   @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a"}\\

   447   @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a\<^sup>\<alpha>"}\\

   411   \end{tabular}

   451   \end{longtable}

   413 

   453   %

   418   This aggregate map-function is necessary if we build quotients, say @{text "(\<alpha>, \<beta>) foo"},

   458   This aggregate map-function is necessary if we build quotients, say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"},

   432   where we already performed some @{text "\<beta>"}-simplifications. In our implementation

   472   where we already performed some @{text "\<beta>"}-simplifications. In our

   433   we further simplified this by noticing the usual laws about @{text "map"}s and @{text "id"},

   473   implementation we further simplify this by noticing the usual laws about

   434   namely @{term "map id = id"} and 

   474   @{text "map"}s and @{text "id"}, namely @{term "map id = id"} and @{text "f

   435   @{text "f \<circ> id = id \<circ> f = f"}. This gives us the simplified abstraction function

   475   \<circ> id = id \<circ> f = f"}. This gives us the simplified abstraction function

   436   

   476 

   444   Apart from the last 2 points the definition is same as the one implemented in

   484   \noindent

   445   in Homeier's HOL package. Adding composition in last two cases is necessary

   485   Note that by using the operator @{text "\<singlearr>"} we do not have to 

   446   for compositional quotients. We illustrate the different behaviour of the

   486   distinguish between arguments and results: teh representation and abstraction

   447   definition by showing the derived definition of @{term fconcat}:

   487   functions are just inverses which we can combine using @{text "\<singlearr>"}.

   448 

   488   So all our definitions are of the general form

   449   @{thm fconcat_def[no_vars]}

   489 

   450 

   490   @{text [display, indent=10] "c \<equiv> ABS (\<sigma>, \<tau>) t"}

   451   The aggregate @{term Abs} function takes a finite set of finite sets

   491 

   452   and applies @{term "map rep_fset"} composed with @{term rep_fset} to

   492   \noindent

   453   its input, obtaining a list of lists, passes the result to @{term concat}

   493   where @{text \<sigma>} is the type of @{text "t"} and @{text "\<tau>"} the type of the 

   454   obtaining a list and applies @{term abs_fset} obtaining the composed

   494   newly defined quotient constant @{text "c"}. To ensure we obtained a correct 

   455   finite set.

   495   definition, we can prove:

   456 

   457   For every type map function we require the property that @{term "map id = id"}.

   458   With this we can compactify the term, removing the identity mappings,

   459   obtaining a definition that is the same as the one provided by Homeier

   460   in the cases where the internal type does not change.

   461 

   462   {\it we should be able to prove}

   471   This lemma fails in the over-simplified abstraction and representation function used

   504   \begin{proof}

   472   in Homeier's quotient package.

   505   By induction of the definitions of @{text "ABS"}, @{text "REP"} and @{text "MAP"}.

   506   \end{proof}

   507   

   508   \noindent

   509   This lemma fails for the abstraction and representation functions used in,

   510   for example, Homeier's quotient package.

   869   The package is part of the standard distribution of Isabelle.

   907 

   908 

   909   The code of the quotient package described here is already included in the

   910   standard distribution of Isabelle.\footnote{Avaiable from

   911   \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is

   912   heavily used in Nominal Isabelle, which provides a convenient reasoning

   913   infrastructure for programming language calculi involving binders.  Earlier

   914   versions of Nominal Isabelle have been used successfully in formalisations

   915   of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08},

   916   Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for

   917   concurrency \cite{BengtsonParow09} and a strong normalisation result for

   918   cut-elimination in classical logic \cite{UrbanZhu08}.

   919