nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:0d561216f1f9
+:816204c76e90
 The paper is organised as follows: Section \ref{sec:prelims} presents briefly
 some necessary preliminaries; Section \ref{sec:type} describes the definitions
 of quotient types and shows how definitions of constants can be made over
-quotient types. Section \ref{sec:resp} introduces the notions of respectfullness
+quotient types. Section \ref{sec:resp} introduces the notions of respectfulness
 and preservation; Section \ref{sec:lift} describes the lifting of theorems;
 Section \ref{sec:examples} presents some examples
 and Section \ref{sec:conc} concludes and compares our results to existing
 work.
 *}
 \noindent
 We can generate a definition for this constant using @{text ABS} and @{text REP}.
 But this constant does \emph{not} respect @{text "\<alpha>"}-equivalence and
 consequently no theorem involving this constant can be lifted to @{text
 "\<alpha>"}-equated lambda terms. Homeier formulates the restrictions in terms of
-the properties of \emph{respectfullness} and \emph{preservation}. We have
+the properties of \emph{respectfulness} and \emph{preservation}. We have
 to slightly extend Homeier's definitions in order to deal with quotient
 compositions.
 To formally define what respectfulness is, we have to first define
 the notion of \emph{aggregate equivalence relations} using @{text REL}:
 we throw the following proof obligation
 @{text [display, indent=10] "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
 %%% PROBLEM I do not yet completely understand the
-%%% form of respectfullness theorems
+%%% form of respectfulness theorems
 %%%\noindent
 %%%if @ {text \<sigma>} and @ {text \<tau>} have no type variables. In case they have, then
 %%%the proof obligation is of the form
 %%%
 %%%@ {text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub>  implies  REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
+%%% ANSWER: The respectfulness theorems never have any quotient assumptions,
+%%% So the commited version is ok.
 \noindent
 %%%where @ {text "\<alpha>s"} are the type variables in @{text \<sigma>} and @{text \<tau>}.
-Homeier calls these proof obligations \emph{respectfullness
+Homeier calls these proof obligations \emph{respectfulness
 theorems}. Before lifting a theorem, we require the user to discharge
-them. And the point with @{text bn} is that the respectfullness theorem
+them. And the point with @{text bn} is that the respectfulness theorem
 looks as follows
 @{text [display, indent=10] "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
 \noindent
 @{text [display, indent=10] "(Rep ---> map Rep ---> map Abs) cons = cons"}
 \noindent
 under the assumption @{text "Quotient R Abs Rep"}.
+%%% 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
 The injection proof starts with an equality between the regularized theorem
 and the injected version. The proof again follows by the structure of the
 two terms, and is defined for a goal being a relation between these two terms.
 \begin{itemize}
-\item For two constants, an appropriate constant respectfullness assumption is used.
+\item For two constants, an appropriate constant respectfulness assumption is used.
 \item For two variables, we use the assumptions proved in regularization.
 \item For two abstractions, they are eta-expanded and beta-reduced.
 \item For two applications, if the right side is an application of
 @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"} we
 can reduce the injected pair using the theorem:
 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;
+We extended the notions of respectfulness and preservation;
 with quotient compositions there is more than one condition needed
 for a constant.
 Our package is modularized, so that single definitions, single
-theorems or single respectfullness conditions etc can be added,
+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.
 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
-some its finer points in the implementation.
+some of its finer points in the implementation.
 *}

changeset 2277	816204c76e90
parent 2276	0d561216f1f9
child 2278	337569f85398