--- a/Quotient-Paper/Paper.thy Mon Jun 14 13:24:22 2010 +0200
+++ b/Quotient-Paper/Paper.thy Mon Jun 14 12:30:08 2010 +0200
@@ -114,7 +114,7 @@
(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
- constructions at hand. But if they have to be done over and over again as in
+ 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.
The purpose of a \emph{quotient package} is to ease the lifting of theorems
@@ -150,7 +150,7 @@
\end{center}
\noindent
- The starting point is an existing type, to which we often refer as the
+ The starting point is an existing type, to which we refer as the
\emph{raw type}, over which an equivalence relation given by the user is
defined. With this input the package introduces a new type, to which we
refer as the \emph{quotient type}. This type comes with an
@@ -194,14 +194,14 @@
quotient packages can deal with such definitions. But what is surprising
that none of them can deal with slightly more complicated definitions involving
\emph{compositions} of quotients. Such compositions are needed for example
- in case of quotienting lists to obtain finite sets and the operator that
+ in case of quotienting lists to yield finite sets and the operator that
flattens lists of lists, defined as follows
@{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]}
\noindent
We expect that the corresponding operator on finite sets, written @{term "fconcat"},
- builds the union of finite sets of finite sets:
+ builds finite unions of finite sets:
@{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
@@ -209,7 +209,7 @@
The quotient package should provide us with a definition for @{text "\<Union>"} in
terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is
that the method used in the existing quotient
- packages of just taking the representation of the arguments and then take
+ packages of just taking the representation of the arguments and then taking
the abstraction of the result is \emph{not} enough. The reason is that case in case
of @{text "\<Union>"} we obtain the incorrect definition
@@ -238,17 +238,19 @@
We are also 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. 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 done in the
- lifting process (this was only hinted at in \cite{Homeier05} and implemented
- as a ``rough recipe'' in ML-code).
+ 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
+ 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} presents the definitions
- of quotient types and shows how definitions can be made over quotient types. \ldots
+ 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
*}
@@ -256,7 +258,7 @@
text {*
In this section we present the definitions of a quotient that follow
- those by Homeier, the proofs can be found there.
+ closely those given by Homeier.
\begin{definition}[Quotient]
A relation $R$ with an abstraction function $Abs$
@@ -282,11 +284,8 @@
then @{thm (concl) fun_quotient[no_vars]}
\end{lemma}
-*}
+ Higher Order Logic
-subsection {* Higher Order Logic *}
-
-text {*
Types:
\begin{eqnarray}\nonumber
@@ -315,9 +314,9 @@
section {* Quotient Types and Quotient Definitions\label{sec:type} *}
text {*
- The first step in a quotient constructions is to take a name for the new
+ The first step in a quotient construction is to take a name for the new
type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},
- defined over a raw type, say @{text "\<sigma>"}. The type of this equivalence
+ defined over a raw type, say @{text "\<sigma>"}. The type of the equivalence
relation must be of type @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of
the declaration is therefore
@@ -341,7 +340,8 @@
which introduce the type of integers and of finite sets using the
equivalence relations @{text "\<approx>\<^bsub>nat \<times> nat\<^esub>"} and @{text
"\<approx>\<^bsub>list\<^esub>"} defined earlier in \eqref{natpairequiv} and
- \eqref{listequiv}, respectively. Given this data, we declare internally
+ \eqref{listequiv}, respectively (the proofs about being equivalence
+ relations is omitted). Given this data, we declare internally
the quotient types as
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -349,10 +349,10 @@
\end{isabelle}
\noindent
- where the right hand side is the (non-empty) set of equivalence classes of
+ where the right-hand side is the (non-empty) set of equivalence classes of
@{text "R"}. The restriction in this declaration is that the type variables
in the raw type @{text "\<sigma>"} must be included in the type variables @{text
- "\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will provide us with
+ "\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will provide us with the following
abstraction and representation functions having the type
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -380,10 +380,11 @@
@{text [display, indent=10] "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
\noindent
- holds (for the proof see \cite{Homeier05}).
+ holds (for the proof see \cite{Homeier05}) for every quotient type defined
+ as above.
- The next step in a quotient construction is to introduce new definitions
- involving the quotient type, which need to be defined in terms of concepts
+ 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
of the raw type (remember this is the only way how to extend HOL
with new definitions). For the user visible is the declaration
@@ -412,12 +413,13 @@
The problem for us is that from such declarations we need to derive proper
definitions using the @{text "Abs"} and @{text "Rep"} functions for the
quotient types involved. The data we rely on is the given quotient type
- @{text "\<tau>"} and the raw type @{text "\<sigma>"}. They allow us to define aggregate
- abstraction and representation functions using the functions @{text "ABS (\<sigma>,
- \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses are given below. The idea behind
- them is to recursively descend into types @{text \<sigma>} and @{text \<tau>}, and generate the appropriate
+ @{text "\<tau>"} and the raw type @{text "\<sigma>"}. They allow us to define \emph{aggregate
+ abstraction} and \emph{representation functions} using the functions @{text "ABS (\<sigma>,
+ \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses we given below. The idea behind
+ these two functions is to recursively descend into the raw types @{text \<sigma>} and
+ quotient types @{text \<tau>}, and generate the appropriate
@{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore
- we return just the identity whenever the types are equal. All clauses
+ we generate just the identity whenever the types are equal. All clauses
are as follows:
\begin{center}
@@ -434,7 +436,7 @@
\multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\
@{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s)))"}\\
@{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s))) \<circ> Rep_\<kappa>\<^isub>q"}
- \end{tabular}
+ \end{tabular}\hfill\numbered{ABSREP}
\end{center}
%
\noindent
@@ -442,7 +444,7 @@
\<kappa>\<^isub>q"} is the quotient of the raw type @{text "\<rho>s \<kappa>"} (for example
@{text "int"} and @{text "nat \<times> nat"}, or @{text "\<alpha> fset"} and @{text "\<alpha>
list"}). The quotient construction ensures that the type variables in @{text
- "\<rho>s"} must be amongst the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
+ "\<rho>s"} must be among the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
matchers for the @{text "\<alpha>s"} when matching @{text "\<rho>s \<kappa>"} against
@{text "\<sigma>s \<kappa>"}. The
function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw
@@ -460,27 +462,29 @@
\noindent
In this definition we abuse the fact that we can interpret type-variables @{text \<alpha>} as
term variables @{text a}. In the last clause we build an abstraction over all
- term-variables inside the aggregate map-function generated by the auxiliary function
+ term-variables inside map-function generated by the auxiliary function
@{text "MAP'"}.
- The need of aggregate map-functions can be appreciated if we build quotients,
- say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types of the form @{text "(\<alpha> list) \<times> \<beta>"}.
- In this case @{text MAP} generates the aggregate map-function:
+ The need of aggregate map-functions can be seen in cases where we build quotients,
+ say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}.
+ In this case @{text MAP} generates the
+ aggregate map-function:
@{text [display, indent=10] "\<lambda>a b. map_prod (map a) b"}
\noindent
which we need to define the aggregate abstraction and representation functions.
- To se how these definitions pan out in practise, let us return to our
- example about @{term "concat"} and @{term "fconcat"}, where we have types
- @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>
- fset"}. Feeding them into @{text ABS} gives us the abstraction function
+ To see how these definitions pan out in practise, let us return to our
+ example about @{term "concat"} and @{term "fconcat"}, where we have the raw type
+ @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and the quotient type @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>
+ fset"}. Feeding them into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)
+ the abstraction function
@{text [display, indent=10] "(map (map id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map id"}
\noindent
- after some @{text "\<beta>"}-simplifications. In our implementation we further
- simplify this abstraction function employing the usual laws about @{text
+ In our implementation we further
+ simplify this function by rewriting with the usual laws about @{text
"map"}s and @{text "id"}, namely @{term "map id = id"} and @{text "f \<circ> id =
id \<circ> f = f"}. This gives us the abstraction function
@@ -492,19 +496,22 @@
@{text [display, indent=10] "\<Union> \<equiv> ((map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}
\noindent
- Note that by using the operator @{text "\<singlearr>"} we do not have to
+ Note that by using the operator @{text "\<singlearr>"} 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 "\<singlearr>"} to deal uniformly with arguments of functions and
- their result. As a result, all definitions in the quotient package
+ their result. Consequently, all definitions in the quotient package
are of the general form
@{text [display, indent=10] "c \<equiv> ABS (\<sigma>, \<tau>) t"}
\noindent
where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the
- type of the defined quotient constant @{text "c"}. To ensure we
- obtained a correct definition, we can prove:
+ 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
+ that the terms involved are all typable.
\begin{lemma}
If @{text "ABS (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"}
@@ -514,20 +521,22 @@
\end{lemma}
\begin{proof}
- By induction and analysing the definitions of @{text "ABS"}, @{text "REP"}
- and @{text "MAP"}. The cases of equal and function types are straightforward
- (the latter follows from @{text "\<singlearr>"} having the type
- @{text "(\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> (\<gamma> \<Rightarrow> \<delta>) \<Rightarrow> (\<beta> \<Rightarrow> \<gamma>) \<Rightarrow> (\<alpha> \<Rightarrow> \<delta>)"}). The case of equal
- type constructors follows by observing that a map-function after applying
- the functions @{text "ABS (\<sigma>s, \<tau>s)"} produce a term of type @{text "\<sigma>s \<kappa> \<Rightarrow> \<tau>s \<kappa>"}.
- The interesting case is the one with unequal type constructors. Since we know the
- quotient is between @{text "\<alpha>s \<kappa>\<^isub>q"} and @{text "\<rho>s \<kappa>"}, we have that @{text "Abs_\<kappa>\<^isub>q"}
- is of type @{text "\<rho>s \<kappa> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"}, that can be more specialised to @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"}
- where the type variables @{text "\<alpha>s"} are instantiated with @{text "\<tau>s"}. The
- complete type can be calculated by observing that @{text "MAP (\<rho>s \<kappa>)"} after applying
- the functions @{text "ABS (\<sigma>s', \<tau>s)"} to it, returns a term of type
- @{text "\<rho>s[\<sigma>s'] \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}. This type is equivalent to @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}
- as desired.\qed
+ By induction and analysing the definitions of @{text "ABS"}, @{text "REP"}
+ and @{text "MAP"}. The cases of equal types and function types are
+ straightforward (the latter follows from @{text "\<singlearr>"} having the
+ type @{text "(\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> (\<gamma> \<Rightarrow> \<delta>) \<Rightarrow> (\<beta> \<Rightarrow> \<gamma>) \<Rightarrow> (\<alpha> \<Rightarrow> \<delta>)"}). In case of equal type
+ constructors we can observe that a map-function after applying the functions
+ @{text "ABS (\<sigma>s, \<tau>s)"} produces a term of type @{text "\<sigma>s \<kappa> \<Rightarrow> \<tau>s \<kappa>"}. The
+ interesting case is the one with unequal type constructors. Since we know
+ the quotient is between @{text "\<alpha>s \<kappa>\<^isub>q"} and @{text "\<rho>s \<kappa>"}, we have
+ that @{text "Abs_\<kappa>\<^isub>q"} is of type @{text "\<rho>s \<kappa> \<Rightarrow> \<alpha>s
+ \<kappa>\<^isub>q"}. This type can be more specialised to @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s
+ \<kappa>\<^isub>q"} where the type variables @{text "\<alpha>s"} are instantiated with the
+ @{text "\<tau>s"}. The complete type can be calculated by observing that @{text
+ "MAP (\<rho>s \<kappa>)"}, after applying the functions @{text "ABS (\<sigma>s', \<tau>s)"} to it,
+ returns a term of type @{text "\<rho>s[\<sigma>s'] \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}. This type is
+ equivalent to @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}, which we just have to compose with
+ @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"} according to the type of @{text "\<circ>"}.\qed
\end{proof}
\noindent
@@ -538,20 +547,30 @@
section {* Respectfulness and Preservation *}
text {*
- Before we can lift theorems involving the raw types to theorems over
- quotient types, we have to impose some restrictions. The reason is that not
- all theorems can be lifted. Homeier formulates these restrictions in terms
- of \emph{respectfullness} and \emph{preservation} of constants occuring in
- theorems.
+ 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 lift process, we need to impose
+ some restrictions. The reason is that even if definitions for all raw constants
+ can be given, \emph{not} all theorems can be actually be lifted. Most notably is
+ the bound variable function, that is the constant @{text bn}, defined for
+ raw lambda-terms as follows
- The respectfulness property for a constant states that it essentially
- respects the equivalence relation involved in the quotient. An example
- is the function returning bound variables of a lambda-term (see \eqref{lambda})
- and @{text "\<alpha>"}-equivalence. It will turn out that this function is not
- respectful.
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "bn (x) \<equiv> \<emptyset>"}\hspace{5mm}
+ @{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{5mm}
+ @{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}
+ \end{isabelle}
- To state the respectfulness property we have to define \emph{aggregate equivalence
- relations}.
+ \noindent
+ This constant just does not respect @{text "\<alpha>"}-equivalence and as
+ consequently no theorem involving this constant can be lifted to @{text
+ "\<alpha>"}-equated lambda terms. Homeier formulates the restrictions in terms of
+ the properties of \emph{respectfullness} and \emph{preservation}. We have
+ to slighlty extend Homeier's definitions in order to deal with quotient
+ compositions.
+
+ To formally define what respectfulness is, we have to first define
+ the notion of \emph{aggregate equivalence relations}.
@{text [display] "GIVE DEFINITION HERE"}