--- 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 (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
- \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"}
+ %%% PROBLEM I do not yet completely understand the
+ %%% form of respectfullness 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"}
\noindent
- where @{text "\<alpha>s"} are the type variables in @{text \<sigma>} and @{text \<tau>}.
+ %%%where @ {text "\<alpha>s"} are the type variables in @{text \<sigma>} and @{text \<tau>}.
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 \<doublearr> rel_list R \<doublearr> rel_listR) append append"}
+ @{text [display, indent=10] "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^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 :: \<sigma>"} and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"},
+ then a preservation theorem is as follows
+
+ @{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"}
+
+ \noindent
+ where the @{text "\<alpha>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] "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^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 \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> 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 \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> 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} *}