# HG changeset patch # User Christian Urban # Date 1276518492 -7200 # Node ID 4bba0d41ff2c39873eec9faf26ad9e0eb410a6d1 # Parent a040404748006a95da56446ce5e8b1a3f68b2be2 tuned diff -r a04040474800 -r 4bba0d41ff2c Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Mon Jun 14 12:30:08 2010 +0200 +++ b/Quotient-Paper/Paper.thy Mon Jun 14 14:28:12 2010 +0200 @@ -113,7 +113,7 @@ from the raw type @{typ "nat \ nat"} to the quotient type @{typ int} (similarly for finite sets and $\alpha$-equated lambda-terms). This lifting usually requires a \emph{lot} of tedious reasoning effort \cite{Paulson06}. - It is feasible to to this work manually, if one has only a few quotient + It is feasible to do this work manually, if one has only a few quotient constructions at hand. But if they have to be done over and over again, as in Nominal Isabelle, then manual reasoning is not an option. @@ -158,7 +158,7 @@ and @{text Rep}.\footnote{Actually slightly more basic functions are given; the functions @{text Abs} and @{text Rep} need to be derived from them. We will show the details later. } These functions relate elements in the - existing type to ones in the new type and vice versa; they can be uniquely + existing type to elements in the new type and vice versa; they can be uniquely identified by their type. For example for the integer quotient construction the types of @{text Abs} and @{text Rep} are @@ -236,21 +236,22 @@ of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation} from Homeier \cite{Homeier05}. - We are also able to address the criticism by Paulson \cite{Paulson06} cited + In addition we are able to address the criticism by Paulson \cite{Paulson06} cited at the beginning of this section about having to collect theorems that are lifted from the raw level to the quotient level into one giant list. Our quotient package is the first one that is modular so that it allows to lift - single theorems separately. This has the advantage for the user to develop a - formal theory interactively an a natural progression. A pleasing result of - the modularity is also that we are able to clearly specify what needs to be + single theorems separately. This has the advantage for the user of being able to develop a + formal theory interactively as a natural progression. A pleasing side-result of + the modularity is that we are able to clearly specify what needs to be done in the lifting process (this was only hinted at in \cite{Homeier05} and implemented as a ``rough recipe'' in ML-code). 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 definition of constants can be made over - quotient types. \ldots + of quotient types and shows how definitions of constants can be made over + quotient types. Section \ref{sec:resp} introduces the notions of respectfullness + and preservation.\ldots *} @@ -376,12 +377,13 @@ respectively. Given that @{text "R"} is an equivalence relation, the following property - - @{text [display, indent=10] "Quotient R Abs_\\<^isub>q Rep_\\<^isub>q"} + \begin{property} + @{text "Quotient R Abs_\\<^isub>q Rep_\\<^isub>q"} + \end{property} \noindent - holds (for the proof see \cite{Homeier05}) for every quotient type defined - as above. + holds for every quotient type defined + as above (for the proof see \cite{Homeier05}). The next step in a quotient construction is to introduce definitions of new constants involving the quotient type. These definitions need to be given in terms of concepts @@ -415,7 +417,7 @@ quotient types involved. The data we rely on is the given quotient type @{text "\"} and the raw type @{text "\"}. They allow us to define \emph{aggregate abstraction} and \emph{representation functions} using the functions @{text "ABS (\, - \)"} and @{text "REP (\, \)"} whose clauses we given below. The idea behind + \)"} and @{text "REP (\, \)"} whose clauses we give below. The idea behind these two functions is to recursively descend into the raw types @{text \} and quotient types @{text \}, and generate the appropriate @{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore @@ -423,6 +425,7 @@ are as follows: \begin{center} + \hfill \begin{tabular}{rcl} \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ @{text "ABS (\, \)"} & $\dn$ & @{text "id :: \ \ \"}\\ @@ -460,7 +463,7 @@ \end{center} % \noindent - In this definition we abuse the fact that we can interpret type-variables @{text \} as + In this definition we rely on the fact that we can interpret type-variables @{text \} as term variables @{text a}. In the last clause we build an abstraction over all term-variables inside map-function generated by the auxiliary function @{text "MAP'"}. @@ -498,10 +501,8 @@ \noindent Note that by using the operator @{text "\"} and special clauses for function types in \eqref{ABSREP}, we do not have to - distinguish between arguments and results: the representation and abstraction - functions are just inverses of each other, which we can combine using - @{text "\"} to deal uniformly with arguments of functions and - their result. Consequently, all definitions in the quotient package + distinguish between arguments and results, but can deal with them uniformly. + Consequently, all definitions in the quotient package are of the general form @{text [display, indent=10] "c \ ABS (\, \) t"} @@ -510,7 +511,7 @@ where @{text \} is the type of the definiens @{text "t"} and @{text "\"} the type of the defined quotient constant @{text "c"}. This data can be easily generated from the declaration given by the user. - To increase the confidence of making correct definitions, we can prove + To increase the confidence in this way of making definitions, we can prove that the terms involved are all typable. \begin{lemma} @@ -544,7 +545,7 @@ functions used, for example, in Homeier's quotient package. *} -section {* Respectfulness and Preservation *} +section {* Respectfulness and Preservation \label{sec:resp} *} text {* The main point of the quotient package is to automatically ``lift'' theorems @@ -556,8 +557,8 @@ raw lambda-terms as follows \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - @{text "bn (x) \ \"}\hspace{5mm} - @{text "bn (t\<^isub>1 t\<^isub>2) \ bn (t\<^isub>1) \ bn (t\<^isub>2)"}\hspace{5mm} + @{text "bn (x) \ \"}\hspace{4mm} + @{text "bn (t\<^isub>1 t\<^isub>2) \ bn (t\<^isub>1) \ bn (t\<^isub>2)"}\hspace{4mm} @{text "bn (\x. t) \ {x} \ bn (t)"} \end{isabelle}