--- a/Quotient-Paper/Paper.thy Fri Jun 11 21:58:25 2010 +0200
+++ b/Quotient-Paper/Paper.thy Sat Jun 12 02:36:49 2010 +0200
@@ -11,8 +11,8 @@
rel_conj ("_ OOO _" [53, 53] 52) and
"op -->" (infix "\<rightarrow>" 100) and
"==>" (infix "\<Rightarrow>" 100) and
- fun_map (infix "\<longrightarrow>" 51) and
- fun_rel (infix "\<Longrightarrow>" 51) and
+ fun_map ("_ \<^raw:\mbox{\tt{---\textgreater}}> _" 51) and
+ fun_rel ("_ \<^raw:\mbox{\tt{===\textgreater}}> _" 51) and
list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
fempty ("\<emptyset>") and
funion ("_ \<union> _") and
@@ -71,18 +71,18 @@
natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations
such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in
terms of operations on pairs of natural numbers (namely @{text
- "add\<^bsub>nat\<times>nat\<^esub> (n\<^isub>1, m\<^isub>1) (n\<^isub>2,
+ "add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2,
m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}).
Similarly one can construct the type of finite sets, written @{term "\<alpha> fset"},
by quotienting the type @{text "\<alpha> list"} according to the equivalence relation
- @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}
+ @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}
\noindent
- which states that two lists are equivalent if every element in one list is also
- member in the other (@{text "\<in>"} stands here for membership in lists). The
- empty finite set, written @{term "{||}"}, can then be defined as the
- empty list and the union of two finite sets, written @{text "\<union>"}, as list append.
+ which states that two lists are equivalent if every element in one list is
+ also member in the other. The empty finite set, written @{term "{||}"}, can
+ then be defined as the empty list and the union of two finite sets, written
+ @{text "\<union>"}, as list append.
An area where quotients are ubiquitous is reasoning about programming language
calculi. A simple example is the lambda-calculus, whose ``raw'' terms are defined as
@@ -131,7 +131,7 @@
\draw ( 0.7, 0.23) node {\begin{tabular}{@ {}c@ {}}equiv-\\[-1mm]clas.\end{tabular}};
\draw (-2.45, 0.35) node {\begin{tabular}{@ {}c@ {}}new\\[-1mm]type\end{tabular}};
\draw (1.8, 0.35) node[right=-0.1mm]
- {\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};
+ {\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw elements)\end{tabular}};
\draw (0.9, -0.55) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
\draw[->, very thick] (-1.8, 0.36) -- (-0.1,0.36);
@@ -145,33 +145,43 @@
\noindent
The starting point is an existing type over which an equivalence relation
given by the user is defined. With this input the package introduces a new
- type, which comes with two associated abstraction and representation
+ type that comes with associated \emph{abstraction} and \emph{representation}
functions, written @{text Abs} and @{text Rep}. These functions relate
- elements in the existing and new type, and can be uniquely identified by
- their type (which however we often omit for better readability). They
- represent an isomorphism between the non-empty subset and elements in the
- new type. They are necessary for making definitions involving the new type. For
- example @{text "0"} and @{text "1"} of type @{typ int} can be defined as
+ elements in the existing type to ones in the new type and vice versa; they
+ can be uniquely identified by their type. For example for the integer
+ quotient construction the types of @{text Abs} and @{text Rep} are
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "Abs::nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep::int \<Rightarrow> nat \<times> nat"}
+ \end{isabelle}
+
+ \noindent
+ However we often leave this typing information implicit for better
+ readability. Every abstraction and representation function represents an
+ isomorphism between the non-empty subset and elements in the new type. They
+ are necessary for making definitions involving the new type. For example
+ @{text "0"} and @{text "1"} of type @{typ int} can be defined as
+
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{text "0 \<equiv> Abs (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs (1, 0)"}
\end{isabelle}
\noindent
- Slightly more complicated is the definition of @{text "add"} which has type
+ Slightly more complicated is the definition of @{text "add"} having type
@{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition is as follows
- @{text [display, indent=10] "add n m \<equiv> Abs (add\<^bsub>nat\<times>nat\<^esub> (Rep n) (Rep m))"}
+ @{text [display, indent=10] "add n m \<equiv> Abs (add_pair (Rep n) (Rep m))"}
\noindent
- where we have to take first the representation of @{text n} and @{text m},
- add them according to @{text "add\<^bsub>nat\<times>nat\<^esub>"} and then take the
+ where we take the representation of the arguments @{text n} and @{text m},
+ add them according to @{text "add_pair"} and then take the
abstraction of the result. This is all straightforward and the existing
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 finite sets. For example over lists one can define an operator
- that flattens lists of lists as follows
+ in case of quotienting lists and the operator that flattens lists of lists, defined
+ as follows
@{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]}
@@ -183,59 +193,51 @@
\noindent
The quotient package should provide us with a definition for @{text "\<Union>"} in
- terms of @{text flat}, @{text Rep} and @{text Abs}. The problem is that it
- is not enough to just take the representation of the argument and then
- take the abstraction of the result, because in that case we obtain an operator
- with type @{text "(\<alpha> list) fset \<Rightarrow> \<alpha> fset"}, not the expected
- @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}. It turns out that we need
- to build aggregate representation and abstraction functions, which in
- case of @{term "fconcat"} produce the following definition
+ terms of @{text flat}, @{text Rep} and @{text Abs} (the latter two having
+ the type @{text "\<alpha> fset \<Rightarrow> \<alpha> list"} and @{text "\<alpha> list \<Rightarrow> \<alpha> fset"},
+ respectively). The problem is that the method is used in the existing quotient
+ packages of just taking the representation of the arguments and then take
+ the abstraction of the result is \emph{not} enough. The reason is that case in case
+ of @{text "\<Union>"} we obtain the incorrect definition
+
+ @{text [display, indent=10] "\<Union> S \<equiv> Abs (flat (Rep S))"}
- @{text [display, indent=10] "\<Union> S \<equiv> Abs (concat ((map Rep \<circ> Rep) S))"}
+ \noindent
+ where the right-hand side is not even typable! This problem can be remedied in the
+ existing quotient packages by introducing an intermediate step and reasoning
+ about faltening of lists of finite sets. However, this remedy is rather
+ cumbersome and inelegant in light of our work, which can deal with such
+ definitions directly. The solution is that we need to build aggregate
+ representation and abstraction functions, which in case of @{text "\<Union>"}
+ generate the following definition
+
+ @{text [display, indent=10] "\<Union> S \<equiv> Abs (flat ((map Rep \<circ> Rep) S))"}
\noindent
where @{term map} is the usual mapping function for lists. In this paper we
- will present a formal definition for our aggregate abstraction and
+ will present a formal definition of our aggregate abstraction and
representation functions (this definition was omitted in \cite{Homeier05}).
- They generate definitions like the one above for @{text add} and @{text "\<Union>"}
+ They generate definitions, like the one above for @{text "\<Union>"},
according to the type of the ``raw'' constant and the type
- of the quotient constant.
+ of the quotient constant. This means we also have to extend the notions
+ of \emph{respectfulness} and \emph{preservation} from Homeier
+ \cite{Homeier05}.
-
+ We will also 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 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 \ldots
*}
-subsection {* Contributions *}
-text {*
- We present the detailed lifting procedure, which was not shown before.
-
- The quotient package presented in this paper has the following
- advantages over existing packages:
- \begin{itemize}
-
- \item We define quotient composition, function map composition and
- relation map composition. This lets lifting polymorphic types with
- subtypes quotiented as well. We extend the notions of
- respectfulness and preservation to cope with quotient
- composition.
- \item We allow lifting only some occurrences of quotiented
- types. Rsp/Prs extended. (used in nominal)
-
- \item The quotient package is very modular. Definitions can be added
- separately, rsp and prs can be proved separately, Quotients and maps
- can be defined separately and theorems can
- be lifted on a need basis. (useful with type-classes).
-
- \item Can be used both manually (attribute, separate tactics,
- rsp/prs databases) and programatically (automated definition of
- lifted constants, the rsp proof obligations and theorem statement
- translation according to given quotients).
-
- \end{itemize}
-*}
-
-section {* General Quotient *}
+section {* Preliminaries and General Quotient\label{sec:prelims} *}
@@ -289,7 +291,7 @@
*}
-section {* Constants *}
+section {* Lifting of Definitions *}
(* Say more about containers? *)
@@ -721,6 +723,43 @@
section {* Conclusion *}
+text {*
+ The package is part of the standard distribution of Isabelle.
+*}
+
+
+subsection {* Contributions *}
+
+text {*
+ We present the detailed lifting procedure, which was not shown before.
+
+ The quotient package presented in this paper has the following
+ advantages over existing packages:
+ \begin{itemize}
+
+ \item We define quotient composition, function map composition and
+ relation map composition. This lets lifting polymorphic types with
+ subtypes quotiented as well. We extend the notions of
+ respectfulness and preservation to cope with quotient
+ composition.
+
+ \item We allow lifting only some occurrences of quotiented
+ types. Rsp/Prs extended. (used in nominal)
+
+ \item The quotient package is very modular. Definitions can be added
+ separately, rsp and prs can be proved separately, Quotients and maps
+ can be defined separately and theorems can
+ be lifted on a need basis. (useful with type-classes).
+
+ \item Can be used both manually (attribute, separate tactics,
+ rsp/prs databases) and programatically (automated definition of
+ lifted constants, the rsp proof obligations and theorem statement
+ translation according to given quotients).
+
+ \end{itemize}
+*}
+
+
(*<*)
end
(*>*)