644   some restrictions in the form of proof obligations that arise during the

   644   two restrictions in the form of proof obligations that arise during the

   694   \noindent

   694   %%% PROBLEM I do not yet completely understand the 

   695   if @{text \<sigma>} and @{text \<tau>} have no type variables. In case they have, then

   695   %%% form of respectfullness theorems

   696   the proof obligation is of the form

   696   %%%\noindent

   697 

   697   %%%if @ {text \<sigma>} and @ {text \<tau>} have no type variables. In case they have, then

   698   @{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"}

   698   %%%the proof obligation is of the form

   699 

   699   %%% 

   700   \noindent

   700   %%%@ {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"}

   701   where @{text "\<alpha>s"} are the type variables in @{text \<sigma>} and @{text \<tau>}.

   701 

   702   \noindent

   703   %%%where @ {text "\<alpha>s"} are the type variables in @{text \<sigma>} and @{text \<tau>}.

   720   @{text [display, indent=10] "(rel_list R \<doublearr> rel_list R \<doublearr> rel_listR) append append"}

   722   @{text [display, indent=10] "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}

   723 

   724   \noindent

   725   To do so, we have to establish

   726   

   727   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   728   if @{thm (prem1) append_rsp_unfolded[of xs ys us vs, no_vars]} and

   729   @{thm (prem2) append_rsp_unfolded[of xs ys us vs, no_vars]}

   730   then @{thm (concl) append_rsp_unfolded[of xs ys us vs, no_vars]} 

   731   \end{isabelle}

   732 

   733   \noindent

   734   which is straightforward given the definition shown in \eqref{listequiv}.

   735 

   736   The second restriction we have to impose arises from

   737   non-lifted polymorphic constants, which are instantiated to a

   738   type being quotient. For example, take the @{term "cons"} to 

   739   add a pair of natural numbers to a list. The pair of natural numbers 

   740   is to become an integer. But we still want to use @{text cons} for

   741   adding integers to lists---just with a different type. 

   742   To be able to lift such theorems, we need a \emph{preservation theorem} 

   743   for @{text cons}. Assuming we have a poplymorphic raw constant 

   744   @{text "c\<^isub>r :: \<sigma>"} and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"}, 

   745   then a preservation theorem is as follows

   746 

   747   @{text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies  ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"}

   748 

   749   \noindent

   750   where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}.

   751   In case of @{text cons} we have 

   752 

   753   @{text [display, indent=10] "(Rep ---> map Rep ---> map Abs) cons = cons"}

   726   class returned by this constant depends only on the equivalence

   759   %%% PROBLEM I do not understand this

   727   classes of the arguments applied to the constant. To automatically

   760   %%%This is not enough to lift theorems that talk about quotient compositions.

   728   lift a theorem that talks about a raw constant, to a theorem about

   761   %%%For some constants (for example empty list) it is possible to show a

   729   the quotient type a respectfulness theorem is required.

   762   %%%general compositional theorem, but for @ {term "op #"} it is necessary

   730 

   763   %%%to show that it respects the particular quotient type:

   731   A respectfulness condition for a constant can be expressed in

   764   %%%

   732   terms of an aggregate relation between the constant and itself,

   765   %%%@ {thm [display, indent=10] insert_preserve2[no_vars]}

   733   for example the respectfullness for @{text "append"}

   766 

   734   can be stated as:

   767   %%% PROBLEM I also do not follow this

   735 

   768   %%%{\it Composition of Quotient theorems}

   736   @{text [display, indent=10] "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}

   769   %%%

   737 

   770   %%%Given two quotients, one of which quotients a container, and the

   738   \noindent

   771   %%%other quotients the type in the container, we can write the

   739   Which after unfolding the definition of @{term "op ===>"} is equivalent to:

   772   %%%composition of those quotients. To compose two quotient theorems

   740 

   773   %%%we compose the relations with relation composition as defined above

   741   @{thm [display, indent=10] append_rsp_unfolded[no_vars]}

   774   %%%and the abstraction and relation functions are the ones of the sub

   742 

   775   %%%quotients composed with the usual function composition.

   743   \noindent An aggregate relation is defined in terms of relation

   776   %%%The @ {term "Rep"} and @ {term "Abs"} functions that we obtain agree

   744   composition, so we define it first:

   777   %%%with the definition of aggregate Abs/Rep functions and the

   745 

   778   %%%relation is the same as the one given by aggregate relations.

   746   

   779   %%%This becomes especially interesting

   747 

   780   %%%when we compose the quotient with itself, as there is no simple

   748   The aggregate relation for an aggregate raw type and quotient type

   781   %%%intermediate step.

   749   is defined as:

   782   %%%

   750 

   783   %%%Lets take again the example of @ {term flat}. To be able to lift

   751 

   784   %%%theorems that talk about it we provide the composition quotient

   752   Again, the last case is novel, so lets look at the example of

   785   %%%theorem which allows quotienting inside the container:

   753   respectfullness for @{term concat}. The statement according to

   786   %%%

   754   the definition above is:

   787   %%%If @ {term R} is an equivalence relation and @ {term "Quotient R Abs Rep"}

   755 

   788   %%%then

   756   @{thm [display, indent=10] concat_rsp[no_vars]}

   789   %%%

   757 

   790   %%%@ {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)"}

   758   \noindent

   791   %%%

   759   By unfolding the definition of relation composition and relation map

   792   %%%\noindent

   760   we can see the equivalent statement just using the primitive list

   793   %%%this theorem will then instantiate the quotients needed in the

   761   equivalence relation:

   794   %%%injection and cleaning proofs allowing the lifting procedure to

   762 

   795   %%%proceed in an unchanged way.

   763   @{thm [display, indent=10] concat_rsp_unfolded[of "a" "a'" "b'" "b", no_vars]}

   764 

   765   The statement reads that, for any lists of lists @{term a} and @{term b}

   766   if there exist intermediate lists of lists @{term "a'"} and @{term "b'"}

   767   such that each element of @{term a} is in the relation with an appropriate

   768   element of @{term a'}, @{term a'} is in relation with @{term b'} and each

   769   element of @{term b'} is in relation with the appropriate element of

   770   @{term b}.

   771 

   772 

   773   Sometimes a non-lifted polymorphic constant is instantiated to a

   774   type being lifted. For example take the @{term "op #"} which inserts

   775   an element in a list of pairs of natural numbers. When the theorem

   776   is lifted, the pairs of natural numbers are to become integers, but

   777   the head constant is still supposed to be the head constant, just

   778   with a different type.  To be able to lift such theorems

   779   automatically, additional theorems provided by the user are

   780   necessary, we call these \emph{preservation} theorems following

   781   Homeier's naming.

   782 

   783   To lift theorems that talk about insertion in lists of lifted types

   784   we need to know that for any quotient type with the abstraction and

   785   representation functions @{text "Abs"} and @{text Rep} we have:

   786 

   787   @{thm [display, indent=10] (concl) cons_prs[no_vars]}

   788 

   789   This is not enough to lift theorems that talk about quotient compositions.

   790   For some constants (for example empty list) it is possible to show a

   791   general compositional theorem, but for @{term "op #"} it is necessary

   792   to show that it respects the particular quotient type:

   793 

   794   @{thm [display, indent=10] insert_preserve2[no_vars]}

   795 

   796   {\it Composition of Quotient theorems}

   797 

   798   Given two quotients, one of which quotients a container, and the

   799   other quotients the type in the container, we can write the

   800   composition of those quotients. To compose two quotient theorems

   801   we compose the relations with relation composition as defined above

   802   and the abstraction and relation functions are the ones of the sub

   803   quotients composed with the usual function composition.

   804   The @{term "Rep"} and @{term "Abs"} functions that we obtain agree

   805   with the definition of aggregate Abs/Rep functions and the

   806   relation is the same as the one given by aggregate relations.

   807   This becomes especially interesting

   808   when we compose the quotient with itself, as there is no simple

   809   intermediate step.

   810 

   811   Lets take again the example of @{term flat}. To be able to lift

   812   theorems that talk about it we provide the composition quotient

   813   theorem which allows quotienting inside the container:

   814 

   815   If @{term R} is an equivalence relation and @{term "Quotient R Abs Rep"}

   816   then

   817 

   818   @{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)"}

   819 

   820   \noindent

   821   this theorem will then instantiate the quotients needed in the

   822   injection and cleaning proofs allowing the lifting procedure to

   823   proceed in an unchanged way.

   824