nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:a1f43d64bde9
+:ba068c04a8d9
 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 to this work manually, if one has only a few quotient
+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
 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 ones in the new type and vice versa; they can be uniquely
+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}\ \ \ \ \ \ \ \ \ \ %%%
 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}.
-We are also able to address the criticism by Paulson \cite{Paulson06} cited
+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 to develop a
+single theorems separately. This has the advantage for the user of being able to develop a
-formal theory interactively an a natural progression. A pleasing result of
+formal theory interactively as a natural progression. A pleasing side-result of
-the modularity is also that we are able to clearly specify what needs to be
+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 definition of constants can be made over
+of quotient types and shows how definitions of constants can be made over
-quotient types. \ldots
+quotient types. Section \ref{sec:resp} introduces the notions of respectfullness
+and preservation.\ldots
 *}
 section {* Preliminaries and General Quotient\label{sec:prelims} *}
 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 [display, indent=10] "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
+@{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
+\end{property}
-\noindent
-holds (for the proof see \cite{Homeier05}) for every quotient type defined
+\noindent
-as above.
+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
 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 given below. The idea behind
+\<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 "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>as. MAP'(\<sigma>)"}
 \end{tabular}
 \end{center}
 %
 \noindent
-In this definition we abuse the fact that we can interpret type-variables @{text \<alpha>} as
+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>"}.
 @{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>"} and special clauses
 for function types in \eqref{ABSREP}, we do not have to
-distinguish between arguments and results: the representation and abstraction
+distinguish between arguments and results, but can deal with them uniformly.
-functions are just inverses of each other, which we can combine using
+Consequently, all definitions in the quotient package
-@{text "\<singlearr>"} to deal uniformly with arguments of functions and
-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"}. This data can be easily
 generated from the declaration given by the user.
-To increase the confidence of making correct definitions, we can prove
+To increase the confidence in this way of making 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"},
 \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 *}
+section {* Respectfulness and Preservation \label{sec:resp} *}
 text {*
 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
 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
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-@{text "bn (x) \<equiv> \<emptyset>"}\hspace{5mm}
+@{text "bn (x) \<equiv> \<emptyset>"}\hspace{4mm}
-@{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{5mm}
+@{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{4mm}
 @{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}
 \end{isabelle}
 \noindent
 This constant just does not respect @{text "\<alpha>"}-equivalence and as

changeset 2255	ba068c04a8d9
parent 2254	a1f43d64bde9
parent 2253	8954dc5ebd52
child 2256	f5f21feaa168