
diff -r 9a560e489c64 -r a0fecce8b244 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Wed Jun 23 22:41:16 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Thu Jun 24 00:27:37 2010 +0100
@@ -13,6 +13,8 @@
 * - what do all preservation theorems look like,
     in particular preservation for quotient
     compositions
+  - explain how Quotient R Abs Rep is proved (j-version)
+  - give an example where precise specification helps (core Haskell in nominal?)
 *)
 
 notation (latex output)
@@ -309,7 +311,7 @@
   procedures showing that one theorem implies another by decomposing the term
   underlying the first theorem.
 
-  Like Homeier, our work relies on map-functions defined for every type
+  Like Homeier's, our work relies on map-functions defined for every type
   constructor taking some arguments, for example @{text map} for lists. Homeier
   describes in \cite{Homeier05} map-functions for products, sums, options and
   also the following map for function types
@@ -390,7 +392,7 @@
   always discharge a proof obligation involving @{text "Quotient"}. Our quotient
   package makes heavy 
   use of this part of Homeier's work including an extension 
-  to deal with compositions of equivalence relations defined as follows:
+  for dealing with compositions of equivalence relations defined as follows:
 
   \begin{definition}[Composition of Relations]
   @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate
@@ -745,17 +747,17 @@
   \noindent
   which is straightforward given the definition shown in \eqref{listequiv}.
 
-  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 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} 
-  for @{text cons}. Assuming we have a polymorphic raw constant 
-  @{text "c\<^isub>r :: \<sigma>"} and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"}, 
-  then a preservation property is as follows
+  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 we assume 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} for @{text
+  cons}. Assuming we have a polymorphic raw constant @{text "c\<^isub>r :: \<sigma>"}
+  and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"}, then a
+  preservation property is as follows
+
 
   @{text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies  ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"}
 
@@ -889,7 +891,7 @@
   \noindent
   In the above definition we omitted the cases for existential quantifiers
   and unique existential quantifiers, as they are very similar to the cases
-  for the universal quantifier. For the third and fourt clause, note that 
+  for the universal quantifier. For the third and fourth clause, note that 
   @{text "\<forall>x. P"} is defined as @{text "\<forall> (\<lambda>x. P)"}.
 
   Next we define the function @{text INJ} which takes as argument
@@ -1068,7 +1070,7 @@
   \end{isabelle}
 
   \noindent
-  This property needs to beproved by the user. It
+  This property needs to be proved 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 as follows:
@@ -1078,7 +1080,7 @@
   \end{isabelle}
 
   \noindent
-  or by using the completely automated stating just:
+  or by using the completely automated mode stating just:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
   \isacommand{thm}~~@{text "add_pair_zero[quot_lifted]"}
@@ -1090,57 +1092,58 @@
   @{text [display, indent=10] "0 + x = x"}
 
   \noindent
+  where @{text x} is of type integer.
   Although seemingly simple, arriving at this result without the help of a quotient
-  package requires a substantial reasoning effort.
+  package requires a substantial reasoning effort (see \cite{Paulson06}).
 *}
 
 section {* Conclusion and Related Work\label{sec:conc}*}
 
 text {*
 
-  The code of the quotient package and the examples described here are
-  already included in the
-  standard distribution of Isabelle.\footnote{Available from
-  \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is
-  heavily used in the new version of Nominal Isabelle, which provides a convenient reasoning
-  infrastructure for programming language calculi involving general binders.  
-  To achieve this, it builds types representing @{text \<alpha>}-equivalent terms.
-  Earlier
-  versions of Nominal Isabelle have been used successfully in formalisations
-  of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08},
-  Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for
-  concurrency \cite{BengtsonParow09} and a strong normalisation result for
-  cut-elimination in classical logic \cite{UrbanZhu08}.
+  The code of the quotient package and the examples described here are already
+  included in the standard distribution of Isabelle.\footnote{Available from
+  \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} The package is
+  heavily used in the new version of Nominal Isabelle, which provides a
+  convenient reasoning infrastructure for programming language calculi
+  involving general binders.  To achieve this, it builds types representing
+  @{text \<alpha>}-equivalent terms.  Earlier versions of Nominal Isabelle have been
+  used successfully in formalisations of an equivalence checking algorithm for
+  LF \cite{UrbanCheneyBerghofer08}, Typed
+  Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
+  \cite{BengtsonParow09} and a strong normalisation result for cut-elimination
+  in classical logic \cite{UrbanZhu08}.
+
 
-  There is a wide range of existing of literature for dealing with
-  quotients in theorem provers.
-  Slotosch~\cite{Slotosch97} implemented a mechanism that automatically
-  defines quotient types for Isabelle/HOL. But he did not include theorem lifting.
-  Harrison's quotient package~\cite{harrison-thesis} is the first one that is
-  able to automatically lift theorems, however only first-order theorems (that is theorems
-  where abstractions, quantifiers and variables do not involve functions that
-  include the quotient type). 
-  There is also some work on quotient types in
-  non-HOL based systems and logical frameworks, including theory interpretations
-  in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, 
-  and setoids in Coq \cite{ChicliPS02}.
-  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
-  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. 
+  There is a wide range of existing literature for dealing with quotients
+  in theorem provers.  Slotosch~\cite{Slotosch97} implemented a mechanism that
+  automatically defines quotient types for Isabelle/HOL. But he did not
+  include theorem lifting.  Harrison's quotient package~\cite{harrison-thesis}
+  is the first one that is able to automatically lift theorems, however only
+  first-order theorems (that is theorems where abstractions, quantifiers and
+  variables do not involve functions that include the quotient type). There is
+  also some work on quotient types in non-HOL based systems and logical
+  frameworks, including theory interpretations in
+  PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, and
+  setoids in Coq \cite{ChicliPS02}.  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
+  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 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.
-  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. 
+
+  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.  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 reasoning infrastructure for alpha-equated terms.
 %%
 %% give an example for this
 %%




