--- a/Quotient-Paper/Paper.thy Tue Jun 15 08:56:13 2010 +0200
+++ b/Quotient-Paper/Paper.thy Tue Jun 15 09:44:16 2010 +0200
@@ -357,6 +357,10 @@
and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]}
\end{proposition}
+ \begin{definition}[Respects]
+ An element @{text "x"} respects a relation @{text "R"} if and only if @{text "R x x"}.
+ \end{definition}
+
\noindent
As a result, Homeier was able to build an automatic prover that can nearly
always discharge a proof obligation involving @{text "Quotient"}. Our quotient
@@ -372,10 +376,12 @@
\end{definition}
\noindent
- Unfortunately, restrictions in HOL's type-system prevent us from stating
- and proving a quotient type theorem, like Proposition \ref{funquot}, for compositions
- of relations. However, we can prove all instances where @{text R\<^isub>1} and
- @{text "R\<^isub>2"} are built up by constituent equivalence relations.
+ Unfortunately a quotient type theorem, like Proposition \ref{funquot}, for
+ the composition of any two quotients in not true (it is not even typable in
+ the HOL type system). However, we can prove useful instances for compatible
+ containers. We will show such example in Section \ref{sec:resp}.
+
+
*}
section {* Quotient Types and Quotient Definitions\label{sec:type} *}
@@ -739,9 +745,12 @@
Lets take again the example of @{term flat}. To be able to lift
theorems that talk about it we provide the composition quotient
- theorem:
+ theorem which allows quotienting inside the container:
- @{thm [display, indent=10] quotient_compose_list[no_vars]}
+ 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
@@ -792,10 +801,10 @@
\begin{tabular}{rcl}
\multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\
@{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma>. REG (t, s)"}\\
- @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
+ @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\
@{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma>. REG (t, s)"}\\
- @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
+ @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{equalities (with same types and different types):}\\
@{text "REG ((op =) : \<sigma>, (op =) : \<sigma>)"} & $\dn$ & @{text "(op =) : \<sigma>"}\\
@{text "REG ((op =) : \<sigma>, (op =) : \<tau>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>) : \<sigma>"}\\
@@ -1036,27 +1045,8 @@
text {*
- Oscar Slotosch~\cite{Slotosch97} implemented a mechanism that automatically
- defines quotient types for Isabelle/HOL. It did not include theorem lifting.
- John 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}.
- Larry 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 Peter Homeier~\cite{Homeier05},
- which is the first one to support lifting of higher order theorems. In
- comparison with this package we explore the notion of composition of quotients,
- which allows lifting constants like @{term "concat"} and theorems about it.
- The HOL4 package requires a big lists of constants, theorems to lift,
- respectfullness conditions as input. Our package is modularized, so that
- single definitions, single theorems or single respectfullness conditions etc
- can be added, which allows a natural use of the quotient package together
- with type-classes and locales.
-
- The code of the quotient package described here is already included in the
+ 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 Nominal Isabelle, which provides a convenient reasoning
@@ -1067,38 +1057,42 @@
concurrency \cite{BengtsonParow09} and a strong normalisation result for
cut-elimination in classical logic \cite{UrbanZhu08}.
-*}
+ Oscar Slotosch~\cite{Slotosch97} implemented a mechanism that automatically
+ defines quotient types for Isabelle/HOL. It did not include theorem lifting.
+ John 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}.
+ Larry 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 Peter Homeier~\cite{Homeier05},
+ which is the first one to support lifting of higher order theorems.
-subsection {* Contributions *}
-
-text {*
- We present the detailed lifting procedure, which was not shown before.
-
- The quotient package presented in this paper has the following
- advantages over existing packages:
- \begin{itemize}
-
- \item We define quotient composition, function map composition and
- relation map composition. This lets lifting polymorphic types with
- subtypes quotiented as well. We extend the notions of
- respectfulness and preservation to cope with quotient
- composition.
+ 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 respectfullness and preservation;
+ with quotient compositions there is more than one condition needed
+ for a constant.
- \item We allow lifting only some occurrences of quotiented
- types. Rsp/Prs extended. (used in nominal)
+ Our package is modularized, so that single definitions, single
+ theorems or single respectfullness 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.
- \item The quotient package is very modular. Definitions can be added
- separately, rsp and prs can be proved separately, Quotients and maps
- can be defined separately and theorems can
- be lifted on a need basis. (useful with type-classes).
-
- \item Can be used both manually (attribute, separate tactics,
- rsp/prs databases) and programatically (automated definition of
- lifted constants, the rsp proof obligations and theorem statement
- translation according to given quotients).
-
- \end{itemize}
+ We allow lifting only some occurrences of quotiented types, which
+ is useful in Nominal. 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