--- a/Quotient-Paper/Paper.thy Fri Oct 29 14:25:50 2010 +0900
+++ b/Quotient-Paper/Paper.thy Fri Oct 29 15:37:24 2010 +0100
@@ -114,14 +114,15 @@
\end{isabelle}
\noindent
- This constructions yields the new type @{typ int} and definitions for @{text
+ This constructions yields the new type @{typ int}, and definitions for @{text
"0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of
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_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"},
+ 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
\begin{isabelle}\ \ \ \ \ %%%
@@ -137,13 +138,12 @@
Quotients are important in a variety of areas, but they are really ubiquitous in
the area of reasoning about programming language calculi. A simple example
is the lambda-calculus, whose raw terms are defined as
-
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "t ::= x | t t | \<lambda>x.t"}\hfill\numbered{lambda}
- \end{isabelle}
-
- \noindent
+ %
+ %\begin{isabelle}\ \ \ \ \ %%%
+ @{text "t ::= x | t t | \<lambda>x.t"}%\hfill\numbered{lambda}
+ %\end{isabelle}
+ %
+ %\noindent
The problem with this definition arises, for instance, when one attempts to
prove formally the substitution lemma \cite{Barendregt81} by induction
over the structure of terms. This can be fiendishly complicated (see
@@ -181,7 +181,7 @@
%%% I wouldn't change it.
\begin{center}
- \mbox{}\hspace{20mm}\begin{tikzpicture}
+ \mbox{}\hspace{20mm}\begin{tikzpicture}[scale=0.9]
%%\draw[step=2mm] (-4,-1) grid (4,1);
\draw[very thick] (0.7,0.3) circle (4.85mm);
@@ -201,20 +201,20 @@
\draw[<-, very thick] (-1.8, 0.16) -- (-0.1,0.16);
\draw (-0.95, 0.26) node[above=0.4mm] {@{text Rep}};
\draw (-0.95, 0.26) node[below=0.4mm] {@{text Abs}};
-
\end{tikzpicture}
\end{center}
\noindent
The starting point is an existing type, to which we refer as the
- \emph{raw type} and over which an equivalence relation given by the user is
- defined. With this input the package introduces a new type, to which we
+ \emph{raw type} and over which an equivalence relation is given by the user.
+ With this input the package introduces a new type, to which we
refer as the \emph{quotient type}. This type comes with an
\emph{abstraction} and a \emph{representation} function, written @{text Abs}
and @{text Rep}.\footnote{Actually slightly more basic functions are given;
the functions @{text Abs} and @{text Rep} need to be derived from them. We
will show the details later. } They relate elements in the
- existing type to elements in the new type and vice versa, and can be uniquely
+ existing type to elements in the new type, % and vice versa,
+ and can be uniquely
identified by their quotient type. For example for the integer quotient construction
the types of @{text Abs} and @{text Rep} are
@@ -262,7 +262,8 @@
\end{isabelle}
\noindent
- where @{text "@"} is the usual list append. We expect that the corresponding
+ where @{text "@"} is %the usual
+ list append. We expect that the corresponding
operator on finite sets, written @{term "fconcat"},
builds finite unions of finite sets:
@@ -290,7 +291,8 @@
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
+ generate the %%%following
+ definition
\begin{isabelle}\ \ \ \ \ %%%
@{text "\<Union> S \<equiv> Abs_fset (flat ((map_list Rep_fset \<circ> Rep_fset) S))"}
@@ -391,7 +393,7 @@
which define equivalence relations in terms of constituent equivalence
relations. For example given two equivalence relations @{text "R\<^isub>1"}
and @{text "R\<^isub>2"}, we can define an equivalence relations over
- products as follows
+ products as %% follows
\begin{isabelle}\ \ \ \ \ %%%
@{text "(R\<^isub>1 \<tripple> R\<^isub>2) (x\<^isub>1, x\<^isub>2) (y\<^isub>1, y\<^isub>2) \<equiv> R\<^isub>1 x\<^isub>1 y\<^isub>1 \<and> R\<^isub>2 x\<^isub>2 y\<^isub>2"}
@@ -481,8 +483,7 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{r@ {\hspace{1mm}}l}
@{text "Quot"} & @{text "(rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>)"}\\
- & @{text "(Abs_fset \<circ> map_list Abs)"}\\
- & @{text "(map_list Rep \<circ> Rep_fset)"}\\
+ & @{text "(Abs_fset \<circ> map_list Abs)"} @{text "(map_list Rep \<circ> Rep_fset)"}\\
\end{tabular}
\end{isabelle}
*}
@@ -606,7 +607,7 @@
\hfill
\begin{tabular}{@ {\hspace{2mm}}l@ {}}
\multicolumn{1}{@ {}l}{equal types:}\\
- @{text "ABS (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\
+ @{text "ABS (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\hspace{5mm}%\\
@{text "REP (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\
\multicolumn{1}{@ {}l}{function types:}\\
@{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} $\dn$ @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
@@ -689,7 +690,7 @@
In our implementation we further
simplify this function by rewriting with the usual laws about @{text
"map"}s and @{text "id"}, for example @{term "map_list id = id"} and @{text "f \<circ> id =
- id \<circ> f = f"}. This gives us the simpler abstraction function
+ id \<circ> f = f"}. This gives us %%%the simpler abstraction function
\begin{isabelle}\ \ \ \ \ %%%
@{text "(map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
@@ -708,12 +709,12 @@
distinguish between arguments and results, but can deal with them uniformly.
Consequently, all definitions in the quotient package
are of the general form
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "c \<equiv> ABS (\<sigma>, \<tau>) t"}
- \end{isabelle}
-
- \noindent
+ %
+ %\begin{isabelle}\ \ \ \ \ %%%
+ \mbox{@{text "c \<equiv> ABS (\<sigma>, \<tau>) t"}}
+ %\end{isabelle}
+ %
+ %\noindent
where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the
type of the defined quotient constant @{text "c"}. This data can be easily
generated from the declaration given by the user.
@@ -757,7 +758,8 @@
two restrictions in 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
- notable is the bound variable function, that is the constant @{text bn}, defined
+ notable is the bound variable function %%, that is the constant @{text bn},
+ defined
for raw lambda-terms as follows
\begin{isabelle}
@@ -790,7 +792,7 @@
\begin{center}
\hfill
\begin{tabular}{l}
- \multicolumn{1}{@ {}l}{equal types:}\\
+ \multicolumn{1}{@ {}l}{equal types:}
@{text "REL (\<sigma>, \<sigma>)"} $\dn$ @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
\multicolumn{1}{@ {}l}{equal type constructors:}\\
@{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
@@ -810,12 +812,12 @@
lift to a theorem where @{text "c\<^isub>r"} is replaced by the corresponding
constant @{text "c\<^isub>q :: \<tau>"} defined over a quotient type. In this situation
we generate the following proof obligation
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
- \end{isabelle}
-
- \noindent
+ %
+ %\begin{isabelle}\ \ \ \ \ %%%
+ @{text "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}.
+ %\end{isabelle}
+ %
+ %\noindent
Homeier calls these proof obligations \emph{respectfulness
theorems}. However, unlike his quotient package, we might have several
respectfulness theorems for one constant---he has at most one.
@@ -826,13 +828,13 @@
Before lifting a theorem, we require the user to discharge
respectfulness proof obligations. In case of @{text bn}
- this obligation is as follows
-
- \begin{isabelle}\ \ \ \ \ %%%
+ this obligation is %%as follows
+ %
+ %\begin{isabelle}\ \ \ \ \ %%%
@{text "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
- \end{isabelle}
-
- \noindent
+ %\end{isabelle}
+ %
+ %\noindent
and the point is that the user cannot discharge it: because it is not true. To see this,
we can just unfold the definition of @{text "\<doublearr>"} \eqref{relfun}
using extensionality to obtain the false statement
@@ -842,8 +844,8 @@
\end{isabelle}
\noindent
- 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
+ In contrast, lifting a theorem about @{text "append"} to a theorem describing
+ the union of finite sets will mean to discharge the proof obligation
\begin{isabelle}\ \ \ \ \ %%%
@{text "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}
@@ -1007,21 +1009,21 @@
%
\begin{center}
\begin{tabular}{@ {}l@ {}}
- \multicolumn{1}{@ {}l@ {}}{abstractions:}\smallskip\\
+ \multicolumn{1}{@ {}l@ {}}{abstractions:}\\%%\smallskip\\
@{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} $\dn$
$\begin{cases}
@{text "\<lambda>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
@{text "\<lambda>x\<^sup>\<sigma> \<in> Resp (REL (\<sigma>, \<tau>)). REG (t, s)"}
- \end{cases}$\smallskip\\
+ \end{cases}$\\%%\smallskip\\
\multicolumn{1}{@ {}l@ {}}{universal quantifiers:}\\
@{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} $\dn$
$\begin{cases}
@{text "\<forall>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
@{text "\<forall>x\<^sup>\<sigma> \<in> Resp (REL (\<sigma>, \<tau>)). REG (t, s)"}
- \end{cases}$\smallskip\\
- \multicolumn{1}{@ {}l@ {}}{equality:}\smallskip\\
+ \end{cases}$\\%%\smallskip\\
+ \multicolumn{1}{@ {}l@ {}}{equality: \hspace{3mm}%%}\smallskip\\
%% REL of two equal types is the equality so we do not need a separate case
- @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} $\dn$ @{text "REL (\<sigma>, \<tau>)"}\smallskip\\
+ @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} $\dn$ @{text "REL (\<sigma>, \<tau>)"}}\smallskip\\
\multicolumn{1}{@ {}l@ {}}{applications, variables and constants:}\\
@{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} $\dn$ @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
@{text "REG (x\<^isub>1, x\<^isub>2)"} $\dn$ @{text "x\<^isub>1"}\\
@@ -1236,13 +1238,13 @@
%%
%% give an example for this
%%
- \medskip
+ \smallskip
\noindent
{\bf Acknowledgements:} We would like to thank Peter Homeier for the many
- discussions about his HOL4 quotient package and explaining to us
- some of its finer points in the implementation. Without his patient
- help, this work would have been impossible.
+ discussions about his HOL4 quotient package.\\[-5mm]% and explaining to us
+ %some of its finer points in the implementation. Without his patient
+ %help, this work would have been impossible.
% \appendix
--- a/Quotient-Paper/document/root.bib Fri Oct 29 14:25:50 2010 +0900
+++ b/Quotient-Paper/document/root.bib Fri Oct 29 15:37:24 2010 +0100
@@ -1,13 +1,13 @@
@inproceedings{Nogin02,
author = {Aleksey Nogin},
title = {Quotient Types: A Modular Approach},
- booktitle = {TPHOLs},
+ booktitle = {Proc.~of the 15th TPHOLs conference},
year = {2002},
pages = {263-280},
- ee = {http://link.springer.de/link/service/series/0558/bibs/2410/24100263.htm},
- crossref = {DBLP:conf/tphol/2002},
- bibsource = {DBLP, http://dblp.uni-trier.de}
+ series = {LNCS},
+ volume = {2646}
}
+
@proceedings{DBLP:conf/tphol/2002,
editor = {Victor Carre{\~n}o and
C{\'e}sar Mu{\~n}oz and
@@ -38,12 +38,11 @@
Loic Pottier and
Carlos Simpson},
title = {{M}athematical {Q}uotients and {Q}uotient {T}ypes in {C}oq},
- booktitle = {TYPES},
+ booktitle = {Proc of the TYPES workshop},
year = {2002},
pages = {95-107},
- ee = {http://link.springer.de/link/service/series/0558/bibs/2646/26460095.htm},
- crossref = {DBLP:conf/types/2002},
- bibsource = {DBLP, http://dblp.uni-trier.de}
+ series = {LNCS},
+ volume = {2646}
}
@proceedings{DBLP:conf/types/2002,
@@ -77,13 +76,13 @@
author = {Oscar Slotosch},
title = {Higher Order Quotients and their Implementation in Isabelle
HOL},
- booktitle = {TPHOLs},
+ booktitle = {Proc.~of the 10th TPHOLs conference},
year = {1997},
pages = {291-306},
- ee = {http://dx.doi.org/10.1007/BFb0028401},
- crossref = {DBLP:conf/tphol/1997},
- bibsource = {DBLP, http://dblp.uni-trier.de}
+ series = {LNCS},
+ volume = {1275}
}
+
@proceedings{DBLP:conf/tphol/1997,
editor = {Elsa L. Gunter and
Amy P. Felty},
@@ -102,13 +101,13 @@
@inproceedings{Homeier05,
author = {Peter V. Homeier},
title = {A Design Structure for Higher Order Quotients},
- booktitle = {TPHOLs},
+ booktitle = {Proc of the 18th TPHOLs conference},
year = {2005},
pages = {130-146},
- ee = {http://dx.doi.org/10.1007/11541868_9},
- crossref = {DBLP:conf/tphol/2005},
- bibsource = {DBLP, http://dblp.uni-trier.de}
+ series = {LNCS},
+ volume = {3603}
}
+
@proceedings{DBLP:conf/tphol/2005,
editor = {Joe Hurd and
Thomas F. Melham},