
diff -r 5e98b3f231a0 -r 084b2b7df98a Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Mon Jun 14 10:14:39 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 11:51:34 2010 +0200
@@ -114,7 +114,7 @@
   (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 to 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 
+  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
@@ -150,7 +150,7 @@
   \end{center}
 
   \noindent
-  The starting point is an existing type, to which we often refer as the
+  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
@@ -194,14 +194,14 @@
   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 obtain finite sets and the operator that 
+  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 the union of finite sets of finite sets:
+  builds the finite unions of finite sets:
 
   @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
 
@@ -209,7 +209,7 @@
   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 take
+  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
 
@@ -238,17 +238,19 @@
 
   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).
+  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 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
+  some necessary preliminaries; Section \ref{sec:type} describes the definitions 
+  of quotient types and shows how definition of constants can be made over 
+  quotient types. \ldots
 *}
 
 
@@ -256,7 +258,7 @@
 
 text {*
   In this section we present the definitions of a quotient that follow
-  those by Homeier, the proofs can be found there.
+  closely those given by Homeier.
 
   \begin{definition}[Quotient]
   A relation $R$ with an abstraction function $Abs$
@@ -282,11 +284,8 @@
   then @{thm (concl) fun_quotient[no_vars]}
   \end{lemma}
 
-*}
+  Higher Order Logic 
 
-subsection {* Higher Order Logic *}
-
-text {*
 
   Types:
   \begin{eqnarray}\nonumber
@@ -315,9 +314,9 @@
 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
+  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 this equivalence
+  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
 
@@ -341,7 +340,8 @@
   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 
+  \eqref{listequiv}, respectively (the proofs about being equivalence
+  relations is omitted).  Given this data, we declare internally 
   the quotient types as
   
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -349,10 +349,10 @@
   \end{isabelle}
 
   \noindent
-  where the right hand side is the (non-empty) set of equivalence classes of
+  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
+  "\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will provide us with the following
   abstraction and representation functions having the type
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -380,10 +380,11 @@
   @{text [display, indent=10] "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
 
   \noindent
-  holds (for the proof see \cite{Homeier05}).
+  holds (for the proof see \cite{Homeier05}) for every quotient type defined
+  as above.
 
-  The next step in a quotient construction is to introduce new definitions
-  involving the quotient type, which need to be defined in terms of concepts
+  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
 
@@ -412,12 +413,13 @@
   The problem for us is that from such declarations we need to derive proper
   definitions using the @{text "Abs"} and @{text "Rep"} functions for the
   quotient types involved. The data we rely on is the given quotient type
-  @{text "\<tau>"} and the raw type @{text "\<sigma>"}.  They allow us to define aggregate
-  abstraction and representation functions using the functions @{text "ABS (\<sigma>,
-  \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses are given below. The idea behind
-  them is to recursively descend into types @{text \<sigma>} and @{text \<tau>}, and generate the appropriate
+  @{text "\<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 given 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 returning just the identity whenever the types are equal. All clauses
+  we generate just the identity whenever the types are equal. All clauses
   are as follows:
 
   \begin{center}
@@ -434,7 +436,7 @@
   \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}
+  \end{tabular}\hfill\numbered{ABSREP}
   \end{center}
   %
   \noindent
@@ -442,7 +444,7 @@
   \<kappa>\<^isub>q"} is the quotient of the raw type @{text "\<rho>s \<kappa>"} (for example
   @{text "int"} and @{text "nat \<times> nat"}, or @{text "\<alpha> fset"} and @{text "\<alpha>
   list"}). The quotient construction ensures that the type variables in @{text
-  "\<rho>s"} must be amongst the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
+  "\<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
@@ -460,27 +462,29 @@
   \noindent
   In this definition we abuse 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 the aggregate map-function generated by the auxiliary function 
+  term-variables inside map-function generated by the auxiliary function 
   @{text "MAP'"}.
-  The need of aggregate map-functions can be appreciated if we build quotients, 
-  say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types of the form @{text "(\<alpha> list) \<times> \<beta>"}. 
-  In this case @{text MAP} generates the aggregate map-function:
+  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 se how these definitions pan out in practise, let us return to our
-  example about @{term "concat"} and @{term "fconcat"}, where we have types
-  @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>
-  fset"}. Feeding them into @{text ABS} gives us the abstraction function
+  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 them 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
-  after some @{text "\<beta>"}-simplifications. In our implementation we further
-  simplify this abstraction function employing the usual laws about @{text
+  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 abstraction function
 
@@ -492,19 +496,22 @@
   @{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>"} we do not have to 
+  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: the representation and abstraction
   functions are just inverses of each other, which we can combine using 
   @{text "\<singlearr>"} to deal uniformly with arguments of functions and 
-  their result. As a result, all definitions in the quotient package 
+  their result. Consequently, all definitions in the quotient package 
   are of the general form
 
   @{text [display, indent=10] "c \<equiv> ABS (\<sigma>, \<tau>) t"}
 
   \noindent
   where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the
-  type of the defined quotient constant @{text "c"}. To ensure we
-  obtained a correct definition, we can prove:
+  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 of making correct definitions, we can prove 
+  that the terms involved are all typable.
 
   \begin{lemma}
   If @{text "ABS (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"} 
@@ -514,20 +521,22 @@
   \end{lemma}
 
   \begin{proof}
-  By induction and analysing the definitions of @{text "ABS"}, @{text "REP"} 
-  and @{text "MAP"}. The cases of equal and function types are straightforward
-  (the latter follows from @{text "\<singlearr>"} having the type
-  @{text "(\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> (\<gamma> \<Rightarrow> \<delta>) \<Rightarrow> (\<beta> \<Rightarrow> \<gamma>) \<Rightarrow> (\<alpha> \<Rightarrow> \<delta>)"}). The case of equal
-  type constructors follows by observing that a map-function after applying 
-  the functions @{text "ABS (\<sigma>s, \<tau>s)"} produce a term of type @{text "\<sigma>s \<kappa> \<Rightarrow> \<tau>s \<kappa>"}.
-  The interesting case is the one with unequal type constructors. Since we know the
-  quotient is between @{text "\<alpha>s \<kappa>\<^isub>q"} and @{text "\<rho>s \<kappa>"}, we have that @{text "Abs_\<kappa>\<^isub>q"}
-  is of type @{text "\<rho>s \<kappa> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"}, that can be more specialised to @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"}
-  where the type variables @{text "\<alpha>s"} are instantiated with @{text "\<tau>s"}. The 
-  complete type can be calculated by observing that @{text "MAP (\<rho>s \<kappa>)"} after applying
-  the functions @{text "ABS (\<sigma>s', \<tau>s)"} to it, returns a term of type 
-  @{text "\<rho>s[\<sigma>s'] \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}. This type is equivalent to  @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"} 
-  as desired.\qed
+  By induction and analysing the definitions of @{text "ABS"}, @{text "REP"}
+  and @{text "MAP"}. 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
@@ -538,20 +547,30 @@
 section {* Respectfulness and Preservation *}
 
 text {*
-  Before we can lift theorems involving the raw types to theorems over
-  quotient types, we have to impose some restrictions. The reason is that not
-  all theorems can be lifted. Homeier formulates these restrictions in terms
-  of \emph{respectfullness} and \emph{preservation} of constants occuring in
-  theorems.
+  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 lift process, we need to impose 
+  some restrictions. The reason is that even if definitions for all raw constants 
+  can be given, \emph{not} all theorems can be actually be lifted. Most notably is
+  the bound variable function, that is the constant @{text bn}, defined for 
+  raw lambda-terms as follows
 
-  The respectfulness property for a constant states that it essentially 
-  respects the equivalence relation involved in the quotient. An example
-  is the function returning bound variables of a lambda-term (see \eqref{lambda})
-  and @{text "\<alpha>"}-equivalence. It will turn out that this function is not 
-  respectful. 
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "bn (x) \<equiv> \<emptyset>"}\hspace{5mm}
+  @{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{5mm}
+  @{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}
+  \end{isabelle}
 
-  To state the respectfulness property we have to define \emph{aggregate equivalence 
-  relations}.
+  \noindent
+  This constant just does not respect @{text "\<alpha>"}-equivalence and as
+  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{respectfullness} and \emph{preservation}. We have
+  to slighlty 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}.
 
   @{text [display] "GIVE DEFINITION HERE"}
 




