nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:e4699a240d2c
+:4ae32dd02d14
 \begin{proposition}\label{funquot}
 @{thm[mode=IfThen] fun_quotient[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"
 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
 package makes heavy
 use of this part of Homeier's work including an extension
 %
 @{thm [mode=Rule, display, indent=10] pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
 \end{definition}
 \noindent
-Unfortunately, restrictions in HOL's type-system prevent us from stating
+Unfortunately a quotient type theorem, like Proposition \ref{funquot}, for
-and proving a quotient type theorem, like Proposition \ref{funquot}, for compositions
+the composition of any two quotients in not true (it is not even typable in
-of relations. However, we can prove all instances where @{text R\<^isub>1} and
+the HOL type system). However, we can prove useful instances for compatible
-@{text "R\<^isub>2"} are built up by constituent equivalence relations.
+containers. We will show such example in Section \ref{sec:resp}.
 *}
 section {* Quotient Types and Quotient Definitions\label{sec:type} *}
 text {*
 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:
+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
 injection and cleaning proofs allowing the lifting procedure to
 proceed in an unchanged way.
 \begin{center}
 \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>"}\\
 \multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables, constants:}\\
 @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} & $\dn$ & @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
 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 Nominal Isabelle, which provides a convenient reasoning
+infrastructure for programming language calculi involving binders.  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}.
 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
+which is the first one to support lifting of higher order theorems.
-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,
+Our quotient package for the first time explore the notion of
-respectfullness conditions as input. Our package is modularized, so that
+composition of quotients, which allows lifting constants like @{term
-single definitions, single theorems or single respectfullness conditions etc
+"concat"} and theorems about it. We defined the composition of
-can be added, which allows a natural use of the quotient package together
+relations and showed examples of compositions of quotients which
-with type-classes and locales.
+allows lifting polymorphic types with subtypes quotiented as well.
+We extended the notions of respectfullness and preservation;
-The code of the quotient package described here is already included in the
+with quotient compositions there is more than one condition needed
-standard distribution of Isabelle.\footnote{Available from
+for a constant.
-\href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is
-heavily used in Nominal Isabelle, which provides a convenient reasoning
+Our package is modularized, so that single definitions, single
-infrastructure for programming language calculi involving binders.  Earlier
+theorems or single respectfullness conditions etc can be added,
-versions of Nominal Isabelle have been used successfully in formalisations
+which allows the use of the quotient package together with
-of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08},
+type-classes and locales. This has the advantage over packages
-Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for
+requiring big lists as input for the user of being able to develop
-concurrency \cite{BengtsonParow09} and a strong normalisation result for
+a theory progressively.
-cut-elimination in classical logic \cite{UrbanZhu08}.
+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
-subsection {* Contributions *}
+and respectfulness proof obligations are used in Nominal. Finally
+we streamlined and showed the detailed lifting procedure, which
-text {*
+has not been presented before.
-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.
-\item We allow lifting only some occurrences of quotiented
-types. Rsp/Prs extended. (used in nominal)
-\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}
 \medskip
 \noindent
 {\bf Acknowledgements:} We would like to thank Peter Homeier for the
 discussions about the HOL4 quotient package and explaining us its

changeset 2270	4ae32dd02d14
parent 2269	e4699a240d2c
parent 2268	1fd6809f5a44
child 2272	bf3a29ea74f6