diff -r 99cf23602d36 -r 69b80ad616c5 Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Wed Jun 16 02:55:52 2010 +0100 +++ b/Quotient-Paper/Paper.thy Wed Jun 16 03:44:10 2010 +0100 @@ -641,7 +641,7 @@ The main point of the quotient package is to automatically ``lift'' theorems involving constants over the raw type to theorems involving constants over the quotient type. Before we can describe this lifting process, we need to impose - some restrictions in the form of proof obligations that arise during the + two restrictions in the form of proof obligations that arise during the lifting. The reason is that even if definitions for all raw constants can be given, \emph{not} all theorems can be lifted to the quotient type. Most notably is the bound variable function, that is the constant @{text bn}, defined @@ -691,14 +691,16 @@ @{text [display, indent=10] "REL (\, \) c\<^isub>r c\<^isub>r"} - \noindent - if @{text \} and @{text \} have no type variables. In case they have, then - the proof obligation is of the form - - @{text [display, indent=10] "Quotient R\<^bsub>\s\<^esub> Abs\<^bsub>\s\<^esub> Rep\<^bsub>\s\<^esub> implies REL (\, \) c\<^isub>r c\<^isub>r"} + %%% PROBLEM I do not yet completely understand the + %%% form of respectfullness theorems + %%%\noindent + %%%if @ {text \} and @ {text \} have no type variables. In case they have, then + %%%the proof obligation is of the form + %%% + %%%@ {text [display, indent=10] "Quotient R\<^bsub>\s\<^esub> Abs\<^bsub>\s\<^esub> Rep\<^bsub>\s\<^esub> implies REL (\, \) c\<^isub>r c\<^isub>r"} \noindent - where @{text "\s"} are the type variables in @{text \} and @{text \}. + %%%where @ {text "\s"} are the type variables in @{text \} and @{text \}. Homeier calls these proof obligations \emph{respectfullness theorems}. Before lifting a theorem, we require the user to discharge them. And the point with @{text bn} is that the respectfullness theorem @@ -717,111 +719,80 @@ In contrast, if we lift a theorem about @{text "append"} to a theorem describing the union of finite sets, then we need to discharge the proof obligation - @{text [display, indent=10] "(rel_list R \ rel_list R \ rel_listR) append append"} + @{text [display, indent=10] "(\\<^bsub>list\<^esub> \ \\<^bsub>list\<^esub> \ \\<^bsub>list\<^esub>) append append"} + + \noindent + To do so, we have to establish + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + if @{thm (prem1) append_rsp_unfolded[of xs ys us vs, no_vars]} and + @{thm (prem2) append_rsp_unfolded[of xs ys us vs, no_vars]} + then @{thm (concl) append_rsp_unfolded[of xs ys us vs, no_vars]} + \end{isabelle} + + \noindent + which is straightforward given the definition shown in \eqref{listequiv}. + + The second restriction we have to impose arises from + non-lifted polymorphic constants, which are instantiated to a + type being quotient. For example, take the @{term "cons"} to + add a pair of natural numbers to a list. The pair of natural numbers + is to become an integer. But we still want to use @{text cons} for + adding integers to lists---just with a different type. + To be able to lift such theorems, we need a \emph{preservation theorem} + for @{text cons}. Assuming we have a poplymorphic raw constant + @{text "c\<^isub>r :: \"} and a corresponding quotient constant @{text "c\<^isub>q :: \"}, + then a preservation theorem is as follows + + @{text [display, indent=10] "Quotient R\<^bsub>\s\<^esub> Abs\<^bsub>\s\<^esub> Rep\<^bsub>\s\<^esub> implies ABS (\, \) c\<^isub>r = c\<^isub>r"} + + \noindent + where the @{text "\s"} stand for the type variables in the type of @{text "c\<^isub>r"}. + In case of @{text cons} we have + + @{text [display, indent=10] "(Rep ---> map Rep ---> map Abs) cons = cons"} \noindent under the assumption @{text "Quotient R Abs Rep"}. - class returned by this constant depends only on the equivalence - classes of the arguments applied to the constant. To automatically - lift a theorem that talks about a raw constant, to a theorem about - the quotient type a respectfulness theorem is required. - - A respectfulness condition for a constant can be expressed in - terms of an aggregate relation between the constant and itself, - for example the respectfullness for @{text "append"} - can be stated as: - - @{text [display, indent=10] "(\\<^bsub>list\<^esub> \ \\<^bsub>list\<^esub> \ \\<^bsub>list\<^esub>) append append"} - - \noindent - Which after unfolding the definition of @{term "op ===>"} is equivalent to: - - @{thm [display, indent=10] append_rsp_unfolded[no_vars]} - - \noindent An aggregate relation is defined in terms of relation - composition, so we define it first: - - - - The aggregate relation for an aggregate raw type and quotient type - is defined as: - - - Again, the last case is novel, so lets look at the example of - respectfullness for @{term concat}. The statement according to - the definition above is: - - @{thm [display, indent=10] concat_rsp[no_vars]} - - \noindent - By unfolding the definition of relation composition and relation map - we can see the equivalent statement just using the primitive list - equivalence relation: - - @{thm [display, indent=10] concat_rsp_unfolded[of "a" "a'" "b'" "b", no_vars]} - - The statement reads that, for any lists of lists @{term a} and @{term b} - if there exist intermediate lists of lists @{term "a'"} and @{term "b'"} - such that each element of @{term a} is in the relation with an appropriate - element of @{term a'}, @{term a'} is in relation with @{term b'} and each - element of @{term b'} is in relation with the appropriate element of - @{term b}. - + %%% 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]} - Sometimes a non-lifted polymorphic constant is instantiated to a - type being lifted. For example take the @{term "op #"} which inserts - an element in a list of pairs of natural numbers. When the theorem - is lifted, the pairs of natural numbers are to become integers, but - the head constant is still supposed to be the head constant, just - with a different type. To be able to lift such theorems - automatically, additional theorems provided by the user are - necessary, we call these \emph{preservation} theorems following - Homeier's naming. - - To lift theorems that talk about insertion in lists of lifted types - we need to know that for any quotient type with the abstraction and - representation functions @{text "Abs"} and @{text Rep} we have: - - @{thm [display, indent=10] (concl) cons_prs[no_vars]} - - 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]} - - {\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 \\\ \\<^bsub>list\<^esub>) (abs_fset \ 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. - + %%% 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 \\\ \\<^bsub>list\<^esub>) (abs_fset \ 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. *} section {* Lifting of Theorems\label{sec:lift} *}