nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:cbffed7d81bd
+:36c9d9e658c7
 also member in the other. The empty finite set, written @{term "{||}"}, can
 then be defined as the empty list and the union of two finite sets, written
 @{text "\<union>"}, as list append.
 An area where quotients are ubiquitous is reasoning about programming language
-calculi. A simple example is the lambda-calculus, whose ``raw'' terms are defined as
+calculi. A simple example is the lambda-calculus, whose raw terms are defined as
 @{text [display, indent=10] "t ::= x | t t | \<lambda>x.t"}
 \noindent
 The problem with this definition arises when one attempts to
 prove formally, for example, the substitution lemma \cite{Barendregt81} by induction
 over the structure of terms. This can be fiendishly complicated (see
 \cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof
-about ``raw'' lambda-terms). In contrast, if we reason about
+about raw lambda-terms). In contrast, if we reason about
 $\alpha$-equated lambda-terms, that means terms quotient according to
 $\alpha$-equivalence, then the reasoning infrastructure provided,
 for example, by Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal
 proof of the substitution lemma almost trivial.
 The difficulty is that in order to be able to reason about integers, finite
 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}
+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
 Nominal Isabelle, then manual reasoning is not an option.
 \end{tikzpicture}
 \end{center}
 \noindent
-The starting point is an existing type over which an equivalence relation
+The starting point is an existing type, often referred to as the
-given by the user is defined. With this input the package introduces a new
+\emph{raw level}, over which an equivalence relation given by the user is
-type that comes with associated \emph{abstraction} and \emph{representation}
+defined. With this input the package introduces a new type, to which we
-functions, written @{text Abs} and @{text Rep}. These functions relate
+refer as the \emph{quotient level}. This type comes with an
-elements in the existing type to ones in the new type and vice versa; they
+\emph{abstraction} and a \emph{representation} function, written @{text Abs}
-can be uniquely identified by their type. For example for the integer
+and @{text Rep}. These functions relate elements in the existing type to
-quotient construction the types of @{text Abs} and @{text Rep} are
+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"}
 \end{isabelle}
 \noindent
 However we often leave this typing information implicit for better
-readability. Every abstraction and representation function represents an
+readability. Every abstraction and representation function stands for an
 isomorphism between the non-empty subset and elements in the new type. They
 are necessary for making definitions involving the new type. For example
 @{text "0"} and @{text "1"} of type @{typ int} can be defined as
 @{text [display, indent=10] "add n m \<equiv> Abs (add_pair (Rep n) (Rep m))"}
 \noindent
 where we take the representation of the arguments @{text n} and @{text m},
-add them according to @{text "add_pair"} and then take the
+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 and the operator that flattens lists of lists, defined
+in case of quotienting lists to obtain finite sets and the operator that
-as follows
+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"},
 \noindent
 The quotient package should provide us with a definition for @{text "\<Union>"} in
 terms of @{text flat}, @{text Rep} and @{text Abs} (the latter two having
 the type @{text "\<alpha> fset \<Rightarrow> \<alpha> list"} and @{text "\<alpha> list \<Rightarrow> \<alpha> fset"},
-respectively). The problem is that the method is used in the existing quotient
+respectively). The problem is that the method  used in the existing quotient
 packages of just taking the representation of the arguments and then take
 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 (flat (Rep S))"}
 \noindent
 where the right-hand side is not even typable! This problem can be remedied in the
 existing quotient packages by introducing an intermediate step and reasoning
-about faltening of lists of finite sets. However, this remedy is rather
+about flattening of lists of finite sets. However, this remedy is rather
 cumbersome and inelegant in light of our work, which can deal with such
 definitions directly. The solution is that we need to build aggregate
 representation and abstraction functions, which in case of @{text "\<Union>"}
 generate the following definition
 \noindent
 where @{term map} is the usual mapping function for lists. In this paper we
 will present a formal definition of our aggregate abstraction and
 representation functions (this definition was omitted in \cite{Homeier05}).
 They generate definitions, like the one above for @{text "\<Union>"},
-according to the type of the ``raw'' constant and the type
+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{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 modular so that it
+level to the quotient level. Our quotient package id 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).

changeset 2226	36c9d9e658c7
parent 2225	cbffed7d81bd
child 2227	42d576c54704