708   theorems}. Before lifting a theorem, we require the user to discharge

   708   theorems}. However, unlike his quotient package, we might have several

   709   respectfulness theorems for one constant---he has at most one.

   710   The reason is that because of our quotient compositions, the types

   711   @{text \<sigma>} and @{text \<tau>} are not completely determined by the type of @{text "c\<^bsub>r\<^esub>"}.

   712   And for every instantiation of the types, we might end up with a 

   713   corresponding respectfulness theorem.

   714 

   715   Before lifting a theorem, we require the user to discharge

   754   In case of @{text cons} we have 

   761   In case of @{text cons} (which has type @{text "\<alpha> \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"}) we have 

   759   under the assumption @{text "Quotient R Abs Rep"}.

   766   under the assumption @{text "Quotient R Abs Rep"}. Interestingly, if we have

   760 

   767   an instance of @{text cons} where the type variable @{text \<alpha>} is instantiated

   761   %%% ANSWER

   768   with @{text "nat \<times> nat"} and we also quotient this type to yield integers,

   762   %%% There are 3 things needed to lift things that involve composition of quotients

   769   then we need to show the corresponding preservation lemma.

   763   %%% - The compositional quotient theorem

   770 

   764   %%% - Compositional respectfullness theorems

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

   765   %%% - and compositional preservation theorems.

   772 

   766   %%% And the case of preservation for nil is special, because we prove some property

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

   767   %%% of all elements in an empty list, so any property is true so we can write it

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

   768   %%% more general, but a version restricted to the particular quotient is true as well

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

   769 

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

   770   %%% PROBLEM I do not understand this

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

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

   778   %quotients composed with the usual function composition.

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

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

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

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

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

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

   775   %%%

   782   %This becomes especially interesting

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

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

   777 

   784   %intermediate step.

   778   %%% PROBLEM I also do not follow this

   785   %

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

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

   780   %%%

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

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

   788   %theorem which allows quotienting inside the container:

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

   789   %

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

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

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

   791   %then

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

   792   % 

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

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

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

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

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

   790   %%%This becomes especially interesting

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

   792   %%%intermediate step.

   793   %%%

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

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

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

   797   %%%

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

   799   %%%then

   800   %%%

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

   813   The main purpose of the quotient package is to lifts an theorem over raw

   805   The main benefit of a quotient package is to lift automatically theorems over raw

   814   types to a theorem over quotient types. We will perform this operation in

   806   types to theorems over quotient types. We will perform this lifting in

   815   three phases. In the following we call these phases \emph{regularization},

   807   three phases, called \emph{regularization},

   816   \emph{injection} and \emph{cleaning} following the names Homeier used

   808   \emph{injection} and \emph{cleaning}.

   817   in his implementation.

   809 

   818 

   810   The purpose of regularization is to change the quantifiers and abstractions

   819   Regularization is supposed to change the quantifications and abstractions

   811   in a ``raw'' theorem to quantifiers over variables that respect the relation

   820   in the theorem to quantification over variables that respect the relation

   812   (Definition \ref{def:respects} states what respects means). The purpose of injection is supposed to add @{term Rep}

   821   (definition \ref{def:respects}). Injection is supposed to add @{term Rep}

  1101   heavily used in Nominal Isabelle, which provides a convenient reasoning

  1092   heavily used in the new version of Nominal Isabelle, which provides a convenient reasoning

  1102   infrastructure for programming language calculi involving binders.  Earlier

  1093   infrastructure for programming language calculi involving binders.  

  1094   To achieve this, it builds types representing @{text \<alpha>}-equivalent terms.

  1095   Earlier

  1110   defines quotient types for Isabelle/HOL. It did not include theorem lifting.

  1105   defines quotient types for Isabelle/HOL. But he did not include theorem lifting.

  1111   Harrison's quotient package~\cite{harrison-thesis} is the first one to

  1106   Harrison's quotient package~\cite{harrison-thesis} is the first one that is

  1112   lift theorems, however only first order. There is work on quotient types in

  1107   able to automatically lift theorems, however only first-order theorems (that is theorems

  1113   non-HOL based systems and logical frameworks, namely theory interpretations

  1108   where abstractions, quantifiers and variables do not involve the quotient type). 

  1114   in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or

  1109   There is also some work on quotient types in

  1115   the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}.

  1110   non-HOL based systems and logical frameworks, including theory interpretations

  1116   Paulson shows a construction of quotients that does not require the

  1111   in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, 

  1117   Hilbert Choice operator, again only first order~\cite{Paulson06}.

  1112   and setoids in Coq \cite{ChicliPS02}.

  1118   The closest to our package is the package for HOL4 by Homeier~\cite{Homeier05},

  1113   Paulson showed a construction of quotients that does not require the

  1119   which is the first one to support lifting of higher order theorems.

  1114   Hilbert Choice operator, but also only first-order theorems to be lifted~\cite{Paulson06}.

  1120 

  1115   The most related work to our package is the package for HOL4 by Homeier~\cite{Homeier05}.

  1121 

  1116   He introduced most of the abstract notions about quotients and also deals with the

  1122   Our quotient package for the first time explore the notion of

  1117   lifting of higher-order theorems. However, he cannot deal with quotient compositions (needed

  1123   composition of quotients, which allows lifting constants like @{term

  1118   for lifting theorems about @{text flat}. Also, a number of his definitions, like @{text ABS},

  1124   "concat"} and theorems about it. We defined the composition of

  1119   @{text REP} and @{text INJ} etc only exist in ML-code. On the other hand, Homeier

  1125   relations and showed examples of compositions of quotients which

  1120   is able to deal with partial quotient constructions, which we have not implemented.

  1126   allows lifting polymorphic types with subtypes quotiented as well.

  1121 

  1127   We extended the notions of respectfulness and preservation;

  1122   One advantage of our package is that it is modular---in the sense that every step

  1128   with quotient compositions there is more than one condition needed

  1123   in the quotient construction can be done independently (see the criticism of Paulson

  1129   for a constant.

  1124   about other quotient packages). This modularity is essential in the context of

  1130 

  1125   Isabelle, which supports type-classes and locales.

  1131   Our package is modularized, so that single definitions, single

  1126 

  1132   theorems or single respectfulness conditions etc can be added,

  1127   Another feature of our quotient package is that when lifting theorems, we can

  1133   which allows the use of the quotient package together with

  1128   precisely specify what the lifted theorem should look like. This feature is

  1134   type-classes and locales. This has the advantage over packages

  1129   necessary, for example, when lifting an inductive principle about two lists.

  1135   requiring big lists as input for the user of being able to develop

  1130   This principle has as the conclusion a predicate of the form @{text "P xs ys"},

  1136   a theory progressively.

  1131   and we can precisely specify whether we want to quotient @{text "xs"} or @{text "ys"},

  1137 

  1132   or both. We found this feature very useful in the new version of Nominal 

  1138   We allow lifting only some occurrences of quotiented types, which

  1133   Isabelle.

  1139   is useful in Nominal Isabelle. The package can be used automatically with

  1140   an attribute, manually with separate tactics for parts of the lifting

  1141   procedure, and programatically. Automated definitions of constants

  1142   and respectfulness proof obligations are used in Nominal. Finally

  1143   we streamlined and showed the detailed lifting procedure, which

  1144   has not been presented before.

  1145