--- 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
%%