
diff -r f170ee51eed2 -r 9a560e489c64 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Wed Jun 23 15:59:43 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Wed Jun 23 22:41:16 2010 +0100
@@ -255,9 +255,9 @@
 
   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 higher-order theorems separately. This has the advantage for the user of being able to develop a
+  lifted from the raw level to the quotient level into one giant list. Homeier's and
+  also our quotient package are modular so that they allow lifting
+  theorems separately. This has the advantage for the user of being able to develop a
   formal theory interactively as a natural progression. A pleasing side-result of
   the modularity is that we are able to clearly specify what is involved
   in the lifting process (this was only hinted at in \cite{Homeier05} and
@@ -299,9 +299,9 @@
   respectively.  The type of a term is often made explicit by writing @{text
   "t :: \<sigma>"}. HOL includes a type @{typ bool} for booleans and the function
   type, written @{text "\<sigma> \<Rightarrow> \<tau>"}. HOL also contains many primitive and defined
-  constants; a primitive constant is equality, with type @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
+  constants; for example, a primitive constant is equality, with type @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
   bool"}, and the identity function with type @{text "id :: \<sigma> \<Rightarrow> \<sigma>"} is
-  defined as @{text "\<lambda>x\<^sup>\<sigma>. x\<^sup>\<sigma>"}).
+  defined as @{text "\<lambda>x\<^sup>\<sigma>. x\<^sup>\<sigma>"}.
 
   An important point to note is that theorems in HOL can be seen as a subset
   of terms that are constructed specially (namely through axioms and proof
@@ -318,7 +318,7 @@
 
   \noindent
   Using this map-function, we can give the following, equivalent, but more 
-  uniform, definition for @{text add} shown in \eqref{adddef}:
+  uniform definition for @{text add} shown in \eqref{adddef}:
 
   @{text [display, indent=10] "add \<equiv> (Rep_int \<singlearr> Rep_int \<singlearr> Abs_int) add_pair"}
 
@@ -374,7 +374,7 @@
   \end{definition}
 
   \noindent
-  The value of this definition is that validity of @{text "Quotient R Abs Rep"} can 
+  The value of this definition lies in the fact that validity of @{text "Quotient R Abs Rep"} can 
   often be proved in terms of the validity of @{text "Quotient"} over the constituent 
   types of @{text "R"}, @{text Abs} and @{text Rep}. 
   For example Homeier proves the following property for higher-order quotient
@@ -403,7 +403,7 @@
   \noindent
   Unfortunately, there are two predicaments with compositions of relations.
   First, a general quotient theorem, like the one given in Proposition \ref{funquot},
-  cannot be stated inside HOL, because of the restriction on types.
+  cannot be stated inside HOL, because of restrictions on types.
   Second, even if we were able to state such a quotient theorem, it
   would not be true in general. However, we can prove specific instances of a
   quotient theorem for composing particular quotient relations.
@@ -515,18 +515,17 @@
   @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"}). 
 
   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
+  definitions using @{text "Abs"} and @{text "Rep"}. 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 give below. The idea behind
+  \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses we shall give below. The idea behind
   these two functions is to simultaneously 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. On the ``way'' down,
   however we might have to use map-functions to let @{text Abs} and @{text Rep} act
   over the appropriate types. In what follows we use the short-hand notation 
-  @{text "ABS (\<sigma>s, \<tau>s)"} to mean @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1)\<dots>ABS (\<sigma>\<^isub>i, \<tau>\<^isub>i)"}; similarly 
+  @{text "ABS (\<sigma>s, \<tau>s)"} to mean @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1)\<dots>ABS (\<sigma>\<^isub>n, \<tau>\<^isub>n)"}; similarly 
   for @{text REP}.
   %
   \begin{center}
@@ -657,7 +656,7 @@
   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 lifting process, we need to impose 
-  two restrictions in the form of proof obligations that arise during the
+  two restrictions in form of proof obligations that arise during the
   lifting. The reason is that even if definitions for all raw constants 
   can be given, \emph{not} all theorems can be lifted to the quotient type. Most 
   notable is the bound variable function, that is the constant @{text bn}, defined 
@@ -699,7 +698,7 @@
   @{text "\<rho>s \<kappa>"}. The @{text "\<sigma>s'"} are determined by matching 
   @{text "\<rho>s \<kappa>"} and @{text "\<sigma>s \<kappa>"}.
 
-  Lets return to the lifting procedure of theorems. Assume we have a theorem
+  Let us return to the lifting procedure of theorems. Assume we have a theorem
   that contains the raw constant @{text "c\<^isub>r :: \<sigma>"} and which we want to
   lift to a theorem where @{text "c\<^isub>r"} is replaced by the corresponding
   constant @{text "c\<^isub>q :: \<tau>"} defined over a quotient type. In this situation 
@@ -717,15 +716,15 @@
   corresponding respectfulness theorem.
 
   Before lifting a theorem, we require the user to discharge
-  respectfulness proof obligations. And the point with @{text bn} is that the respectfulness theorem
-  looks as follows
+  respectfulness proof obligations. In case of @{text bn}
+  this obligation is as follows
 
   @{text [display, indent=10] "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
 
   \noindent
-  and the user cannot discharge it: because it is not true. To see this,
+  and the point is that the user cannot discharge it: because it is not true. To see this,
   we can just unfold the definition of @{text "\<doublearr>"} \eqref{relfun} 
-  using extensionally to obtain
+  using extensionally to obtain the false statement
 
   @{text [display, indent=10] "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 implies bn(t\<^isub>1) = bn(t\<^isub>2)"}
  
@@ -749,8 +748,8 @@
   The second restriction we have to impose arises from
   non-lifted polymorphic constants, which are instantiated to a
   type being quotient. For example, take the @{term "cons"}-constructor to 
-  add a pair of natural numbers to a list, whereby teh pair of natural numbers 
-  is to become an integer in te quotient construction. The point is that we 
+  add a pair of natural numbers to a list, whereby the pair of natural numbers 
+  turns into an integer in the quotient construction. The point is that we 
   still want to use @{text cons} for
   adding integers to lists---just with a different type. 
   To be able to lift such theorems, we need a \emph{preservation property} 
@@ -815,7 +814,7 @@
   in a ``raw'' theorem to quantifiers over variables that respect the relation
   (Definition \ref{def:respects} states what respects means). The purpose of injection is to add @{term Rep}
   and @{term Abs} of appropriate types in front of constants and variables
-  of the raw type so that they can be replaced by the ones that include the
+  of the raw type so that they can be replaced by the corresponding constants from the
   quotient type. The purpose of cleaning is to bring the theorem derived in the
   first two phases into the form the user has specified. Abstractly, our
   package establishes the following three proof steps:
@@ -932,7 +931,7 @@
   In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always 
   start with an implication. Isabelle provides \emph{mono} rules that can split up 
   the implications into simpler implicational subgoals. This succeeds for every
-  monotone connective, except in places where the function @{text REG} inserted,
+  monotone connective, except in places where the function @{text REG} replaced,
   for instance, a quantifier by a bounded quantifier. In this case we have 
   rules of the form
 
@@ -947,27 +946,27 @@
   @{text [display, indent=10] "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}    
 
   \noindent
-  And when @{term R\<^isub>2} is an equivalence relation and we can prove
+  If @{term R\<^isub>2} is an equivalence relation, we can prove
 
   @{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
 
   \noindent
   The last theorem is new in comparison with Homeier's package. There the
-  injection procedure would be used to prove such goals, and 
+  injection procedure would be used to prove such goals and 
   the assumption about the equivalence relation would be used. We use the above theorem directly,
   because this allows us to completely separate the first and the second
   proof step into two independent ``units''.
 
   The second proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"},  starts with an equality. 
   The proof again follows the structure of the
-  two underlying terms, and is defined for a goal being a relation between these two terms.
+  two underlying terms and is defined for a goal being a relation between these two terms.
 
   \begin{itemize}
-  \item For two constants an appropriate constant respectfulness lemma is applied.
+  \item For two constants an appropriate respectfulness theorem is applied.
   \item For two variables, we use the assumptions proved in the regularization step.
   \item For two abstractions, we @{text "\<eta>"}-expand and @{text "\<beta>"}-reduce them.
   \item For two applications, we check that the right-hand side is an application of
-    @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"}. If yes then we
+    @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"} holds. If yes then we
     can apply the theorem:
 
     @{term [display, indent=10] "R x y \<longrightarrow> R x (Rep (Abs y))"}
@@ -994,7 +993,7 @@
 
   \noindent
   Next, relations over lifted types are folded to equalities.
-  For this the following theorem has been shown in Homeier~\cite{Homeier05}:
+  For this the following theorem has been shown by  Homeier~\cite{Homeier05}:
 
     @{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]}
 
@@ -1009,15 +1008,12 @@
 
 text {*
 
-  In this section we will show, a complete interaction with the quotient package
-  for defining the type of integers by quotienting pairs of natural numbers and
-  lifting theorems to integers. Our quotient package is fully compatible with
-  Isabelle type classes, but for clarity we will not use them in this example.
-  In a larger formalization of integers using the type class mechanism would
-  provide many algebraic properties ``for free''.
+  In this section we will show a sequence of declarations for defining the 
+  type of integers by quotienting pairs of natural numbers, and
+  lifting one theorem. 
 
   A user of our quotient package first needs to define a relation on
-  the raw type, by which the quotienting will be performed. We give
+  the raw type with which the quotienting will be performed. We give
   the same integer relation as the one presented in \eqref{natpairequiv}:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
@@ -1028,9 +1024,9 @@
   \end{isabelle}
 
   \noindent
-  Next the quotient type is defined. This generates a proof obligation that the
+  Next the quotient type must be defined. This generates a proof obligation that the
   relation is an equivalence relation, which is solved automatically using the
-  definition and extensionality:
+  definition of equivalence and extensionality:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
   \begin{tabular}{@ {}l}
@@ -1060,7 +1056,7 @@
   \end{isabelle}
 
   \noindent
-  If the user attempts to lift this theorem, all proof obligations are 
+  If the user lifts this theorem, all proof obligations are 
   automatically discharged, except the respectfulness
   proof for @{text "add_pair"}:
 
@@ -1072,16 +1068,17 @@
   \end{isabelle}
 
   \noindent
-  This can be discharged automatically by Isabelle when telling it to unfold the definition
+  This property needs to beproved by the user. It
+  can be discharged automatically by Isabelle when hinting to unfold the definition
   of @{text "\<doublearr>"}.
-  After this, the user can prove the lifted lemma explicitly:
+  After this, the user can prove the lifted lemma as follows:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
   \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting add_pair_zero"}
   \end{isabelle}
 
   \noindent
-  or by the completely automated mode by stating:
+  or by using the completely automated stating just:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
   \isacommand{thm}~~@{text "add_pair_zero[quot_lifted]"}
@@ -1130,22 +1127,17 @@
   Paulson showed a construction of quotients that does not require the
   Hilbert Choice operator, but also only first-order theorems can be lifted~\cite{Paulson06}.
   The most related work to our package is the package for HOL4 by Homeier~\cite{Homeier05}.
-  He introduced most of the abstract notions about quotients and also deals with the
+  He introduced most of the abstract notions about quotients and also deals with
   lifting of higher-order theorems. However, he cannot deal with quotient compositions (needed
   for lifting theorems about @{text flat}). Also, a number of his definitions, like @{text ABS},
   @{text REP} and @{text INJ} etc only exist in \cite{Homeier05} as ML-code, not included
   in the paper. 
 
-  One advantage of our package is that it is modular---in the sense that every step
-  in the quotient construction can be done independently (see the criticism of Paulson
-  about other quotient packages). This modularity is essential in the context of
-  Isabelle, which supports type-classes and locales.
-
-  Another feature of our quotient package is that when lifting theorems, teh user can
+  One feature of our quotient package is that when lifting theorems, the user can
   precisely specify what the lifted theorem should look like. This feature is
   necessary, for example, when lifting an induction principle for two lists.
-  This principle has as the conclusion a predicate of the form @{text "P xs ys"},
-  and we can precisely specify whether we want to quotient @{text "xs"} or @{text "ys"},
+  Assuming this principle has as the conclusion a predicate of the form @{text "P xs ys"},
+  then we can precisely specify whether we want to quotient @{text "xs"} or @{text "ys"},
   or both. We found this feature very useful in the new version of Nominal 
   Isabelle, where such a choice is required to generate a resoning infrastructure
   for alpha-equated terms. 




