--- a/Quotient-Paper/Paper.thy Wed Jun 16 14:26:23 2010 +0200
+++ b/Quotient-Paper/Paper.thy Wed Jun 16 22:29:42 2010 +0100
@@ -705,7 +705,14 @@
\noindent
%%%where @ {text "\<alpha>s"} are the type variables in @{text \<sigma>} and @{text \<tau>}.
Homeier calls these proof obligations \emph{respectfulness
- theorems}. Before lifting a theorem, we require the user to discharge
+ theorems}. However, unlike his quotient package, we might have several
+ respectfulness theorems for one constant---he has at most one.
+ The reason is that because of our quotient compositions, the types
+ @{text \<sigma>} and @{text \<tau>} are not completely determined by the type of @{text "c\<^bsub>r\<^esub>"}.
+ And for every instantiation of the types, we might end up with a
+ corresponding respectfulness theorem.
+
+ Before lifting a theorem, we require the user to discharge
them. And the point with @{text bn} is that the respectfulness theorem
looks as follows
@@ -751,54 +758,39 @@
\noindent
where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}.
- In case of @{text cons} we have
+ In case of @{text cons} (which has type @{text "\<alpha> \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"}) we have
@{text [display, indent=10] "(Rep ---> map Rep ---> map Abs) cons = cons"}
\noindent
- under the assumption @{text "Quotient R Abs Rep"}.
+ under the assumption @{text "Quotient R Abs Rep"}. Interestingly, if we have
+ an instance of @{text cons} where the type variable @{text \<alpha>} is instantiated
+ with @{text "nat \<times> nat"} and we also quotient this type to yield integers,
+ then we need to show the corresponding preservation lemma.
- %%% ANSWER
- %%% There are 3 things needed to lift things that involve composition of quotients
- %%% - The compositional quotient theorem
- %%% - Compositional respectfullness theorems
- %%% - and compositional preservation theorems.
- %%% And the case of preservation for nil is special, because we prove some property
- %%% of all elements in an empty list, so any property is true so we can write it
- %%% more general, but a version restricted to the particular quotient is true as well
-
- %%% PROBLEM I do not understand this
- %%%This is not enough to lift theorems that talk about quotient compositions.
- %%%For some constants (for example empty list) it is possible to show a
- %%%general compositional theorem, but for @ {term "op #"} it is necessary
- %%%to show that it respects the particular quotient type:
- %%%
- %%%@ {thm [display, indent=10] insert_preserve2[no_vars]}
+ @{thm [display, indent=10] insert_preserve2[no_vars]}
- %%% PROBLEM I also do not follow this
- %%%{\it Composition of Quotient theorems}
- %%%
- %%%Given two quotients, one of which quotients a container, and the
- %%%other quotients the type in the container, we can write the
- %%%composition of those quotients. To compose two quotient theorems
- %%%we compose the relations with relation composition as defined above
- %%%and the abstraction and relation functions are the ones of the sub
- %%%quotients composed with the usual function composition.
- %%%The @ {term "Rep"} and @ {term "Abs"} functions that we obtain agree
- %%%with the definition of aggregate Abs/Rep functions and the
- %%%relation is the same as the one given by aggregate relations.
- %%%This becomes especially interesting
- %%%when we compose the quotient with itself, as there is no simple
- %%%intermediate step.
- %%%
- %%%Lets take again the example of @ {term flat}. To be able to lift
- %%%theorems that talk about it we provide the composition quotient
- %%%theorem which allows quotienting inside the container:
- %%%
- %%%If @ {term R} is an equivalence relation and @ {term "Quotient R Abs Rep"}
- %%%then
- %%%
- %%%@ {text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep o rep_fset)"}
+ %Given two quotients, one of which quotients a container, and the
+ %other quotients the type in the container, we can write the
+ %composition of those quotients. To compose two quotient theorems
+ %we compose the relations with relation composition as defined above
+ %and the abstraction and relation functions are the ones of the sub
+ %quotients composed with the usual function composition.
+ %The @ {term "Rep"} and @ {term "Abs"} functions that we obtain agree
+ %with the definition of aggregate Abs/Rep functions and the
+ %relation is the same as the one given by aggregate relations.
+ %This becomes especially interesting
+ %when we compose the quotient with itself, as there is no simple
+ %intermediate step.
+ %
+ %Lets take again the example of @ {term flat}. To be able to lift
+ %theorems that talk about it we provide the composition quotient
+ %theorem which allows quotienting inside the container:
+ %
+ %If @ {term R} is an equivalence relation and @ {term "Quotient R Abs Rep"}
+ %then
+ %
+ %@ {text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep o rep_fset)"}
%%%
%%%\noindent
%%%this theorem will then instantiate the quotients needed in the
@@ -810,15 +802,14 @@
text {*
- The main purpose of the quotient package is to lifts an theorem over raw
- types to a theorem over quotient types. We will perform this operation in
- three phases. In the following we call these phases \emph{regularization},
- \emph{injection} and \emph{cleaning} following the names Homeier used
- in his implementation.
+ The main benefit of a quotient package is to lift automatically theorems over raw
+ types to theorems over quotient types. We will perform this lifting in
+ three phases, called \emph{regularization},
+ \emph{injection} and \emph{cleaning}.
- Regularization is supposed to change the quantifications and abstractions
- in the theorem to quantification over variables that respect the relation
- (definition \ref{def:respects}). Injection is supposed to add @{term Rep}
+ The purpose of regularization is to change the quantifiers and abstractions
+ in a ``raw'' theorem to quantifiers over variables that respect the relation
+ (Definition \ref{def:respects} states what respects means). The purpose of injection is supposed to add @{term Rep}
and @{term Abs} of appropriate types in front of constants and variables
of the raw type so that they can be replaced by the ones that include the
quotient type. Cleaning rewrites the obtained injected theorem with
@@ -1098,52 +1089,50 @@
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 Nominal Isabelle, which provides a convenient reasoning
- infrastructure for programming language calculi involving binders. Earlier
+ heavily used in the new version of Nominal Isabelle, which provides a convenient reasoning
+ infrastructure for programming language calculi involving 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. It did not include theorem lifting.
- Harrison's quotient package~\cite{harrison-thesis} is the first one to
- lift theorems, however only first order. There is work on quotient types in
- non-HOL based systems and logical frameworks, namely theory interpretations
- in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or
- the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}.
- Paulson shows a construction of quotients that does not require the
- Hilbert Choice operator, again only first order~\cite{Paulson06}.
- The closest to our package is the package for HOL4 by Homeier~\cite{Homeier05},
- which is the first one to support lifting of higher order theorems.
-
+ 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 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 to 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 the
+ 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 ML-code. On the other hand, Homeier
+ is able to deal with partial quotient constructions, which we have not implemented.
- Our quotient package for the first time explore the notion of
- composition of quotients, which allows lifting constants like @{term
- "concat"} and theorems about it. We defined the composition of
- relations and showed examples of compositions of quotients which
- allows lifting polymorphic types with subtypes quotiented as well.
- We extended the notions of respectfulness and preservation;
- with quotient compositions there is more than one condition needed
- for a constant.
+ One advantage of our package is that it is modular---in the sense that every step
+ in the quotient construction can be done independently (see the criticism of Paulson
+ about other quotient packages). This modularity is essential in the context of
+ Isabelle, which supports type-classes and locales.
- Our package is modularized, so that single definitions, single
- theorems or single respectfulness conditions etc can be added,
- which allows the use of the quotient package together with
- type-classes and locales. This has the advantage over packages
- requiring big lists as input for the user of being able to develop
- a theory progressively.
+ Another feature of our quotient package is that when lifting theorems, we can
+ precisely specify what the lifted theorem should look like. This feature is
+ necessary, for example, when lifting an inductive principle about two lists.
+ This principle has as the conclusion a predicate of the form @{text "P xs ys"},
+ and 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.
+ \medskip
- We allow lifting only some occurrences of quotiented types, which
- is useful in Nominal Isabelle. The package can be used automatically with
- an attribute, manually with separate tactics for parts of the lifting
- procedure, and programatically. Automated definitions of constants
- and respectfulness proof obligations are used in Nominal. Finally
- we streamlined and showed the detailed lifting procedure, which
- has not been presented before.
-
- \medskip
\noindent
{\bf Acknowledgements:} We would like to thank Peter Homeier for the
discussions about his HOL4 quotient package and explaining to us