nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:5e98b3f231a0
+:084b2b7df98a
 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 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
 and automate the reasoning as much as possible. In the
 context of HOL, there have been a few quotient packages already
 \end{tikzpicture}
 \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
 \emph{abstraction} and a \emph{representation} function, written @{text Abs}
 and @{text Rep}.\footnote{Actually slightly more basic functions are given;
 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 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]}
 \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 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
 @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}
 of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}
 from Homeier \cite{Homeier05}.
 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
+lifted from the raw level to the quotient level into one giant list. Our
-first one that is modular so that it allows to lift single theorems
+quotient package is the first one that is modular so that it allows to lift
-separately. This has the advantage for the user to develop a formal theory
+single theorems separately. This has the advantage for the user to develop a
-interactively an a natural progression. A pleasing result of the modularity
+formal theory interactively an a natural progression. A pleasing result of
-is also that we are able to clearly specify what needs to be done in the
+the modularity is also that we are able to clearly specify what needs to be
-lifting process (this was only hinted at in \cite{Homeier05} and implemented
+done in the lifting process (this was only hinted at in \cite{Homeier05} and
-as a ``rough recipe'' in ML-code).
+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
+some necessary preliminaries; Section \ref{sec:type} describes the definitions
-of quotient types and shows how definitions can be made over quotient types. \ldots
+of quotient types and shows how definition of constants 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.
+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{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
-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)}
 *}
 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
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}
 \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
+\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
+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}\ \ \ \ \ \ \ \ \ \ %%%
 @{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}
 @{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
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~~\isacommand{is}~~@{text "t :: \<sigma>"}
 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
+@{text "\<tau>"} and the raw type @{text "\<sigma>"}.  They allow us to define \emph{aggregate
-abstraction and representation functions using the functions @{text "ABS (\<sigma>,
+abstraction} and \emph{representation functions} using the functions @{text "ABS (\<sigma>,
-\<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses are given below. The idea behind
+\<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses we given below. The idea behind
-them is to recursively descend into types @{text \<sigma>} and @{text \<tau>}, and generate the appropriate
+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}
 \begin{tabular}{rcl}
 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
 @{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}
+\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 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
 type as follows:
 %
 \end{center}
 %
 \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,
+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 of the form @{text "(\<alpha> list) \<times> \<beta>"}.
+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:
+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
+To see how these definitions pan out in practise, let us return to our
-example about @{term "concat"} and @{term "fconcat"}, where we have types
+example about @{term "concat"} and @{term "fconcat"}, where we have the raw type
-@{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>
+@{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 the abstraction function
+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
+In our implementation we further
-simplify this abstraction function employing the usual laws about @{text
+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
 @{text [display, indent=10] "(map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
 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>"} 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
+type of the defined quotient constant @{text "c"}. This data can be easily
-obtained a correct definition, we can prove:
+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"}
 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}
 \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
+and @{text "MAP"}. The cases of equal types and function types are
-(the latter follows from @{text "\<singlearr>"} having the type
+straightforward (the latter follows from @{text "\<singlearr>"} having the
-@{text "(\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> (\<gamma> \<Rightarrow> \<delta>) \<Rightarrow> (\<beta> \<Rightarrow> \<gamma>) \<Rightarrow> (\<alpha> \<Rightarrow> \<delta>)"}). The case of equal
+type @{text "(\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> (\<gamma> \<Rightarrow> \<delta>) \<Rightarrow> (\<beta> \<Rightarrow> \<gamma>) \<Rightarrow> (\<alpha> \<Rightarrow> \<delta>)"}). In case of equal type
-type constructors follows by observing that a map-function after applying
+constructors we can observe that a map-function after applying the functions
-the functions @{text "ABS (\<sigma>s, \<tau>s)"} produce a term of type @{text "\<sigma>s \<kappa> \<Rightarrow> \<tau>s \<kappa>"}.
+@{text "ABS (\<sigma>s, \<tau>s)"} produces a term of type @{text "\<sigma>s \<kappa> \<Rightarrow> \<tau>s \<kappa>"}.  The
-The interesting case is the one with unequal type constructors. Since we know the
+interesting case is the one with unequal type constructors. Since we know
-quotient is between @{text "\<alpha>s \<kappa>\<^isub>q"} and @{text "\<rho>s \<kappa>"}, we have that @{text "Abs_\<kappa>\<^isub>q"}
+the quotient is between @{text "\<alpha>s \<kappa>\<^isub>q"} and @{text "\<rho>s \<kappa>"}, we have
-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"}
+that @{text "Abs_\<kappa>\<^isub>q"} is of type @{text "\<rho>s \<kappa> \<Rightarrow> \<alpha>s
-where the type variables @{text "\<alpha>s"} are instantiated with @{text "\<tau>s"}. The
+\<kappa>\<^isub>q"}. This type can be more specialised to @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s
-complete type can be calculated by observing that @{text "MAP (\<rho>s \<kappa>)"} after applying
+\<kappa>\<^isub>q"} where the type variables @{text "\<alpha>s"} are instantiated with the
-the functions @{text "ABS (\<sigma>s', \<tau>s)"} to it, returns a term of type
+@{text "\<tau>s"}. The complete type can be calculated by observing that @{text
-@{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>"}
+"MAP (\<rho>s \<kappa>)"}, after applying the functions @{text "ABS (\<sigma>s', \<tau>s)"} to it,
-as desired.\qed
+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, for example, in Homeier's quotient package.
 *}
 section {* Respectfulness and Preservation *}
 text {*
-Before we can lift theorems involving the raw types to theorems over
+The main point of the quotient package is to automatically ``lift'' theorems
-quotient types, we have to impose some restrictions. The reason is that not
+involving constants over the raw type to theorems involving constants over
-all theorems can be lifted. Homeier formulates these restrictions in terms
+the quotient type. Before we can describe this lift process, we need to impose
-of \emph{respectfullness} and \emph{preservation} of constants occuring in
+some restrictions. The reason is that even if definitions for all raw constants
-theorems.
+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
-The respectfulness property for a constant states that it essentially
+raw lambda-terms as follows
-respects the equivalence relation involved in the quotient. An example
-is the function returning bound variables of a lambda-term (see \eqref{lambda})
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-and @{text "\<alpha>"}-equivalence. It will turn out that this function is not
+@{text "bn (x) \<equiv> \<emptyset>"}\hspace{5mm}
-respectful.
+@{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)"}
-To state the respectfulness property we have to define \emph{aggregate equivalence
+\end{isabelle}
-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"}
 class returned by this constant depends only on the equivalence
 classes of the arguments applied to the constant. To automatically

changeset 2247	084b2b7df98a
parent 2243	5e98b3f231a0
child 2248	a04040474800