diff -r 92b9b8d2888d -r d003938cc952 Quotient-Paper-jv/Paper.thy
--- a/Quotient-Paper-jv/Paper.thy	Tue Mar 20 11:26:10 2012 +0000
+++ b/Quotient-Paper-jv/Paper.thy	Wed Mar 21 20:34:04 2012 +0000
@@ -50,21 +50,21 @@
 
 text {*
   \noindent
-  One might think quotients have been studied to death, but in the context of
-  theorem provers many questions concerning them are far from settled. In
-  this paper we address the question of how to establish a convenient reasoning
-  infrastructure
-  for quotient constructions in the Isabelle/HOL
-  theorem prover. Higher-Order Logic (HOL) consists
-  of a small number of axioms and inference rules over a simply-typed
-  term-language. Safe reasoning in HOL is ensured by two very restricted
-  mechanisms for extending the logic: one is the definition of new constants
-  in terms of existing ones; the other is the introduction of new types by
-  identifying non-empty subsets in existing types. Previous work has shown how
-  to use both mechanisms for dealing with quotient constructions in HOL (see
-  \cite{Homeier05,Paulson06}).  For example the integers in Isabelle/HOL are
-  constructed by a quotient construction over the type @{typ "nat \<times> nat"} and
-  the equivalence relation
+  One might think quotients have been studied to death, but in the
+  context of theorem provers a number questions concerning them are
+  far from settled. In this paper we address the question of how to
+  establish a convenient reasoning infrastructure for quotient
+  constructions in the Isabelle/HOL theorem prover. Higher-Order Logic
+  (HOL) consists of a small number of axioms and inference rules over
+  a simply-typed term-language. Safe reasoning in HOL is ensured by
+  two very restricted mechanisms for extending the logic: one is the
+  definition of new constants in terms of existing ones; the other is
+  the introduction of new types by identifying non-empty subsets in
+  existing types. Previous work has shown how to use both mechanisms
+  for dealing with quotient constructions in HOL (see
+  \cite{Homeier05,Paulson06}).  For example the integers in
+  Isabelle/HOL are constructed by a quotient construction over the
+  type @{typ "nat \<times> nat"} and the equivalence relation
 
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -83,39 +83,43 @@
   \end{isabelle}
 
   \noindent
-  Similarly one can construct the type of
-  finite sets, written @{term "\<alpha> fset"},
-  by quotienting the type @{text "\<alpha> list"} according to the equivalence relation
+  Similarly one can construct the type of finite sets, written @{term
+  "\<alpha> fset"}, by quotienting the type @{text "\<alpha> list"} according to the
+  equivalence relation
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{text "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}\hfill\numbered{listequiv}
   \end{isabelle}
 
   \noindent
-  which states that two lists are equivalent if every element in one list is
-  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.
+  which states that two lists are equivalent if every element in one
+  list is also member in the other, and vice versa. 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.
 
   Quotients are important in a variety of areas, but they are really ubiquitous in
   the area of reasoning about programming language calculi. A simple example
-  is the lambda-calculus, whose raw terms are defined as
+  is the lambda-calculus, whose raw, or un-quotient, terms are defined as
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{text "t ::= x | t t | \<lambda>x.t"}%\hfill\numbered{lambda}
   \end{isabelle}
 
   \noindent
-  The problem with this definition arises, for instance, when one attempts to
-  prove formally 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
-  $\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 problem with this definition arises from the need to reason
+  modulo $\alpha$-equivalence, for instance, when one attempts to
+  prove formally 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 $\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 fundamental reason is that in case of
+  $\alpha$-equated terms, equality coincides with $\alpha$-equivalence and
+  we can use for reasoning HOL's built-in notion of ``replacing equals by equals''.
 
   {\bf MAYBE AN EAMPLE FOR PARTIAL QUOTIENTS?}