
diff -r b8dda31890ff -r d1ab5d2d6926 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Sun Jun 13 17:41:07 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Sun Jun 13 20:54:50 2010 +0200
@@ -49,7 +49,7 @@
   {\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 popular generic theorem prover in which many logics can be
@@ -64,7 +64,9 @@
   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 + m\<^isub>2 = m\<^isub>1 + n\<^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
@@ -77,7 +79,9 @@
   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
 
-  @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}
+  \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
@@ -145,15 +149,16 @@
 
   \noindent
   The starting point is an existing type, often referred to as the \emph{raw
-  type}, over which an equivalence relation given by the user is
-  defined. With this input the package introduces a new type, to which we
-  refer as the \emph{quotient type}. This type comes with an
-  \emph{abstraction} and a \emph{representation} function, written @{text Abs}
-  and @{text Rep}.\footnote{Actually they need to be derived from slightly
-  more basic functions. We will show the details later. } These functions
-  relate elements in the existing type to ones in the new type and vice versa;
-  they can be uniquely identified by their type. For example for the integer
-  quotient construction the types of @{text Abs} and @{text Rep} are
+  type}, over which an equivalence relation given by the user is defined. With
+  this input the package introduces a new type, to which we refer as the
+  \emph{quotient type}. This type comes with an \emph{abstraction} and a
+  \emph{representation} function, written @{text Abs} and @{text
+  Rep}.\footnote{Actually slightly more basic functions are given; the @{text Abs}
+  and @{text Rep} need to be derived from them. We will show the details
+  later. } These functions relate elements in the existing type to ones in the
+  new type and vice versa; they can be uniquely identified by their type. For
+  example for the integer quotient construction the types of @{text Abs} and
+  @{text Rep} are
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   @{text "Abs :: nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep :: int \<Rightarrow> nat \<times> nat"}
@@ -225,27 +230,27 @@
   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 relation}, \emph{respectfulness} and \emph{preservation}
+  of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}
   from Homeier \cite{Homeier05}.
 
-  We will also 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. 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 to develop a formal theory interactively an a natural progression. A
-  pleasing result of the modularity is also 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 \ldots
+  We are also 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. 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 to develop a formal theory
+  interactively an a natural progression. A pleasing result of the modularity
+  is also 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} presents the definitions 
+  of quotient types and shows how definitions can be made over quotient types. \ldots
 *}
 
 
-
 section {* Preliminaries and General Quotient\label{sec:prelims} *}
 
-
-
 text {*
   In this section we present the definitions of a quotient that follow
   those by Homeier, the proofs can be found there.
@@ -296,9 +301,13 @@
 
   {\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.
+
 *}
 
-section {* Quotient Types and Lifting of Definitions *}
+section {* Quotient Types and Quotient Definitions\label{sec:type} *}
 
 text {*
   The first step in a quotient constructions is to take a name for the new
@@ -312,19 +321,34 @@
   \end{isabelle}
 
   \noindent
-  and a proof that @{text "R"} is indeed an equivalence relation.
-  Given this data, we can internally declare the quotient type as
+  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.  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
-  being 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 abstraction and
-  representation functions having the type
+  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
+  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"}
@@ -341,39 +365,54 @@
   
   \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
+  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
+
 
   @{text [display, indent=10] "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
 
   \noindent
   holds (for the proof see \cite{Homeier05}).
 
-  The next step is to lift definitions over the raw type to definitions over the
-  quotient type. For this we provide the declaration
+  The next step is to introduce new definitions involving the quotient type,
+  which need to be defined in terms of concepts of the raw type (remember this 
+  is the only way how toe be able to extend HOL with new definitions). For the
+  user visible is the declaration
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~\isacommand{is}~@{text "c' :: \<sigma>"}
+  \isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~~\isacommand{is}~~@{text "t :: \<sigma>"}
   \end{isabelle}
 
-  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.
+  \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 examples are
 
-  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}\ \ \ \ \ \ \ \ \ \ %%%
+  \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 aggregate abstraction and representation functions
+  using the functions @{text "ABS (\<sigma>, \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose 
+  clauses are given below. The idea behind them is to recursively descend into 
+  both types and generate the appropriate @{text "Abs"} and @{text "Rep"} 
+  in places where the types differ. Therefore we returning just the identity
+  whenever the types are equal.
 
-  {\it the first argument is the raw type and the second argument the quotient type}
-  %
   \begin{center}
   \begin{longtable}{rcl}
   \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ 
@@ -387,35 +426,36 @@
   @{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"}\\
+  @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s'))) \<circ> Rep_\<kappa>\<^isub>q"}
   \end{longtable}
   \end{center}
   %
   \noindent
-  where in the last two clauses we have that the quotient type @{text "\<alpha>s \<kappa>\<^isub>q"} is a quotient of
-  the raw type @{text "\<rho>s \<kappa>"} (for example @{text "\<alpha> fset"} and @{text "\<alpha> list"}). 
-  The quotient construction ensures that the type variables in @{text "\<rho>s"} 
-  must be amongst the @{text "\<alpha>s"}. Now the @{text "\<sigma>s'"} are given by the matchers 
-  for the @{text "\<alpha>s"} 
-  when matching  @{text "\<sigma>s \<kappa>\<^isub>q"} against @{text "\<alpha>s \<kappa>\<^isub>q"}; similarly the @{text "\<tau>s'"} are given by the 
-  same type-variables when matching @{text "\<tau>s \<kappa>"} against @{text "\<rho>s \<kappa>"}.
-  The function @{text "MAP"} calculates an \emph{aggregate map-function} for a type 
-  as follows:
-
+  where in the last two clauses we have that the quotient type @{text "\<alpha>s
+  \<kappa>\<^isub>q"} is a quotient of the raw type @{text "\<rho>s \<kappa>"} (for example
+  @{text "int"} and @{text "nat \<times> nat"}, or @{text "\<alpha> fset"} and @{text "\<alpha>
+  list"}). The quotient construction ensures that the type variables in @{text
+  "\<rho>s"} must be amongst the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
+  matchers for the @{text "\<alpha>s"} when matching @{text "\<sigma>s \<kappa>\<^isub>q"} against
+  @{text "\<alpha>s \<kappa>\<^isub>q"}; similarly the @{text "\<tau>s'"} are given by the same
+  type-variables when matching @{text "\<tau>s \<kappa>"} against @{text "\<rho>s \<kappa>"}.  The
+  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"}\\
+  \begin{longtable}{rcl}
+  @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a\<^sup>\<alpha>"}\\
   @{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id"}\\
   @{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{longtable}
   \end{center}
-
+  %
   \noindent
   In this definition we abuse the fact that we can interpret type-variables @{text \<alpha>} as 
   term variables @{text a}, and in the last clause build an abstraction over all
   term-variables inside the aggregate map-function generated by @{text "MAP'"}.
-  This aggregate map-function is necessary if we build quotients, say @{text "(\<alpha>, \<beta>) foo"},
+  This aggregate map-function is necessary if we build quotients, say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"},
   out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}. In this case @{text MAP}
   generates the aggregate map-function:
 
@@ -429,11 +469,11 @@
   @{text [display, indent=10] "(map (map id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map id"}
 
   \noindent
-  where we already performed some @{text "\<beta>"}-simplifications. In our implementation
-  we further simplified this by noticing the usual laws about @{text "map"}s and @{text "id"},
-  namely @{term "map id = id"} and 
-  @{text "f \<circ> id = id \<circ> f = f"}. This gives us the simplified abstraction function
-  
+  where we already performed some @{text "\<beta>"}-simplifications. In our
+  implementation we further simplify this by noticing the usual laws about
+  @{text "map"}s and @{text "id"}, namely @{term "map id = id"} and @{text "f
+  \<circ> id = id \<circ> f = f"}. This gives us the simplified abstraction function
+
   @{text [display, indent=10] "(map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
 
   \noindent
@@ -441,25 +481,18 @@
 
   @{text [display, indent=10] "\<Union> \<equiv> ((map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}
 
-  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 illustrate the different behaviour of the
-  definition by showing the derived definition of @{term fconcat}:
-
-  @{thm fconcat_def[no_vars]}
+  \noindent
+  Note that by using the operator @{text "\<singlearr>"} we do not have to 
+  distinguish between arguments and results: teh representation and abstraction
+  functions are just inverses which we can combine using @{text "\<singlearr>"}.
+  So all our definitions are of the general form
 
-  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.
+  @{text [display, indent=10] "c \<equiv> ABS (\<sigma>, \<tau>) t"}
 
-  For every type map function we require the property that @{term "map id = id"}.
-  With this we can compactify the term, removing the identity mappings,
-  obtaining a definition that is the same as the one provided by Homeier
-  in the cases where the internal type does not change.
-
-  {\it we should be able to prove}
+  \noindent
+  where @{text \<sigma>} is the type of @{text "t"} and @{text "\<tau>"} the type of the 
+  newly defined quotient constant @{text "c"}. To ensure we obtained a correct 
+  definition, we can prove:
 
   \begin{lemma}
   If @{text "ABS (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"} 
@@ -468,8 +501,13 @@
   @{text "\<tau> \<Rightarrow> \<sigma>"}.
   \end{lemma}
 
-  This lemma fails in the over-simplified abstraction and representation function used
-  in Homeier's quotient package.
+  \begin{proof}
+  By induction of the definitions of @{text "ABS"}, @{text "REP"} and @{text "MAP"}.
+  \end{proof}
+  
+  \noindent
+  This lemma fails for the abstraction and representation functions used in,
+  for example, Homeier's quotient package.
 *}
 
 subsection {* Respectfulness *}
@@ -866,7 +904,19 @@
 section {* Conclusion *}
 
 text {*
-  The package is part of the standard distribution of Isabelle.
+
+
+  The code of the quotient package described here is already included in the
+  standard distribution of Isabelle.\footnote{Avaiable from
+  \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is
+  heavily used in Nominal Isabelle, which provides a convenient reasoning
+  infrastructure for programming language calculi involving binders.  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}.
+
 *}
 
 




