| author | Christian Urban <urbanc@in.tum.de> |
| Sat, 29 May 2010 00:16:39 +0200 | |
| changeset 2202 | bdbf040dce89 |
| parent 2174 | 157e8a4a6556 |
| child 2205 | 69b4eb4b12c6 |
| permissions | -rw-r--r-- |
|
2174
157e8a4a6556
changed qpaper to lncs-style
Christian Urban <urbanc@in.tum.de>
parents:
2032
diff
changeset
|
1 |
%\documentclass{svjour3}
|
|
157e8a4a6556
changed qpaper to lncs-style
Christian Urban <urbanc@in.tum.de>
parents:
2032
diff
changeset
|
2 |
\documentclass{llncs}
|
|
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
\usepackage{times}
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
\usepackage{isabelle}
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
\usepackage{isabellesym}
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
\usepackage{amsmath}
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
\usepackage{amssymb}
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
\usepackage{pdfsetup}
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
\urlstyle{rm}
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
\isabellestyle{it}
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
\renewcommand{\isastyle}{\isastyleminor}
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
\begin{document}
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
|
|
2032
5641981ec67d
some preliminary notes of the abstract (qpaper); still need to see the motivating example
Christian Urban <urbanc@in.tum.de>
parents:
1975
diff
changeset
|
17 |
\title{Quotients Revisited for Isabelle/HOL}
|
|
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
\author{Cezary Kaliszyk$^*$ and Christian Urban$^*$}
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
\institute{$^*$ Technical University of Munich, Germany}
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
\maketitle |
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
\begin{abstract}
|
|
2202
bdbf040dce89
first version of the abstract
Christian Urban <urbanc@in.tum.de>
parents:
2174
diff
changeset
|
23 |
Higher-order logic (HOL) is based on a small logic kernel, whose |
|
bdbf040dce89
first version of the abstract
Christian Urban <urbanc@in.tum.de>
parents:
2174
diff
changeset
|
24 |
only mechanism for extension is the introduction of definitions |
|
bdbf040dce89
first version of the abstract
Christian Urban <urbanc@in.tum.de>
parents:
2174
diff
changeset
|
25 |
and types. Both extensions are often performed by |
|
bdbf040dce89
first version of the abstract
Christian Urban <urbanc@in.tum.de>
parents:
2174
diff
changeset
|
26 |
quotient constructions, for example finite sets are constructed by quotienting |
|
bdbf040dce89
first version of the abstract
Christian Urban <urbanc@in.tum.de>
parents:
2174
diff
changeset
|
27 |
lists, or integers by quotienting pairs of natural numbers. To ease the work |
|
bdbf040dce89
first version of the abstract
Christian Urban <urbanc@in.tum.de>
parents:
2174
diff
changeset
|
28 |
involved with quotient construction, we re-implemented in Isabelle/HOL |
|
bdbf040dce89
first version of the abstract
Christian Urban <urbanc@in.tum.de>
parents:
2174
diff
changeset
|
29 |
the quotient package by Homeier. In doing so we extended his work |
|
bdbf040dce89
first version of the abstract
Christian Urban <urbanc@in.tum.de>
parents:
2174
diff
changeset
|
30 |
in order to deal with compositions of quotients. Also, we designed |
|
bdbf040dce89
first version of the abstract
Christian Urban <urbanc@in.tum.de>
parents:
2174
diff
changeset
|
31 |
our quotient package so that every step in a quotient construction |
|
bdbf040dce89
first version of the abstract
Christian Urban <urbanc@in.tum.de>
parents:
2174
diff
changeset
|
32 |
can be performed separately. |
|
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
\end{abstract}
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
34 |
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
35 |
% generated text of all theories |
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
36 |
\input{session}
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
38 |
% optional bibliography |
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
39 |
\bibliographystyle{abbrv}
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
40 |
\bibliography{root}
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
42 |
\end{document}
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
43 |
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
%%% Local Variables: |
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
45 |
%%% mode: latex |
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
46 |
%%% TeX-master: t |
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
47 |
%%% End: |