--- 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.
-
-*}
-
+*)
(*<*)