
diff -r bf4b28ebb412 -r ea0cdb7c6455 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Thu Oct 28 15:16:43 2010 +0900
+++ b/Quotient-Paper/Paper.thy	Fri Oct 29 14:25:50 2010 +0900
@@ -315,8 +315,8 @@
   sketch this part of our work in Section 5 and we defer the reader to a longer
   version for the details. However, we will give in Section 3 and 4 all 
   definitions that specify the input and output data of our three-step 
-  lifting procedure. Section 6 gives an example how our quotient package
-  works in practise. 
+  lifting procedure.
+  %Appendix A gives an example how our quotient package works in practise.
 *}
 
 section {* Preliminaries and General\\ Quotients\label{sec:prelims} *}
@@ -1179,8 +1179,76 @@
   %in two equal terms that can be solved by reflexivity.
 *}
 
+section {* Conclusion and Related Work\label{sec:conc}*}
 
-section {* Examples \label{sec:examples} *}
+text {*
+
+  \noindent
+  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 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.
+  Like Homeier's, our quotient package can deal with partial equivalence
+  relations, but for lack of space we do not describe the mechanisms
+  needed for this kind of quotient constructions.
+
+%%% FIXME Reviewer 3 would like to know more about the lifting in Coq and PVS,
+%%% and some comparison. I don't think we have the space for any additions...
+
+  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
+%%
+  \medskip
+
+  \noindent
+  {\bf Acknowledgements:} We would like to thank Peter Homeier for the many
+  discussions about his HOL4 quotient package and explaining to us
+  some of its finer points in the implementation. Without his patient
+  help, this work would have been impossible.
+
+%  \appendix
+
+*}
+
+(* section {* Examples \label{sec:examples} *}
 
 text {*
 
@@ -1189,7 +1257,7 @@
 %%% it due to lack of space...
 
   \noindent
-  In this section we will show a sequence of declarations for defining the 
+  In this appendix we will show a sequence of declarations for defining the 
   type of integers by quotienting pairs of natural numbers, and
   lifting one theorem. 
 
@@ -1271,74 +1339,7 @@
   Although seemingly simple, arriving at this result without the help of a quotient
   package requires a substantial reasoning effort (see \cite{Paulson06}).
 *}
-
-section {* Conclusion and Related Work\label{sec:conc}*}
-
-text {*
-
-  \noindent
-  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 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.
-  Like Homeier's, our quotient package can deal with partial equivalence
-  relations, but for lack of space we do not describe the mechanisms
-  needed for this kind of quotient constructions.
-
-%%% FIXME Reviewer 3 would like to know more about the lifting in Coq and PVS,
-%%% and some comparison. I don't think we have the space for any additions...
-
-  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
-%%
-  \medskip
-
-  \noindent
-  {\bf Acknowledgements:} We would like to thank Peter Homeier for the many
-  discussions about his HOL4 quotient package and explaining to us
-  some of its finer points in the implementation. Without his patient
-  help, this work would have been impossible.
-
-*}
-
+*)
 
 
 (*<*)




