10 |
10 |
11 \urlstyle{rm} |
11 \urlstyle{rm} |
12 \isabellestyle{it} |
12 \isabellestyle{it} |
13 \renewcommand{\isastyle}{\isastyleminor} |
13 \renewcommand{\isastyle}{\isastyleminor} |
14 |
14 |
|
15 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
|
16 \renewcommand{\isasymequiv}{$\dn$} |
|
17 \renewcommand{\isasymemptyset}{$\varnothing$} |
|
18 |
15 \begin{document} |
19 \begin{document} |
16 |
20 |
17 \title{Quotients Revisited for Isabelle/HOL} |
21 \title{Quotients Revisited for Isabelle/HOL} |
18 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$} |
22 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$} |
19 \institute{$^*$ Technical University of Munich, Germany} |
23 \institute{$^*$ Technical University of Munich, Germany} |
20 \maketitle |
24 \maketitle |
21 |
25 |
22 \begin{abstract} |
26 \begin{abstract} |
23 Higher-order logic (HOL) is based on a small logic kernel, whose |
27 Higher-order logic (HOL), used in several theorem provers, is based on a |
24 only mechanism for extension is the introduction of definitions |
28 small logic kernel, whose only mechanism for extension is the introduction |
25 and types. Both extensions are often performed by |
29 of safe definitions and non-empty types. Both extensions are often performed by |
26 quotient constructions, for example finite sets are constructed by quotienting |
30 quotient constructions; for example finite sets are constructed by quotienting |
27 lists, or integers by quotienting pairs of natural numbers. To ease the work |
31 lists, or integers by quotienting pairs of natural numbers. To ease the work |
28 involved with quotient constructions, we re-implemented in Isabelle/HOL |
32 involved with quotient constructions, we re-implemented in Isabelle/HOL |
29 the quotient package by Homeier. In doing so we extended his work |
33 the quotient package by Homeier. In doing so we extended his work |
30 in order to deal with compositions of quotients. Also, we designed |
34 in order to deal with compositions of quotients. Also, we designed |
31 our quotient package so that every step in a quotient construction |
35 our quotient package so that every step in a quotient construction |
32 can be performed separately. |
36 can be performed separately. The importance to programming language research |
|
37 is that many properties of programming languages are more convenient to verify |
|
38 over $\alpha$-quotient terms, than over raw terms. |
33 \end{abstract} |
39 \end{abstract} |
34 |
40 |
35 % generated text of all theories |
41 % generated text of all theories |
36 \input{session} |
42 \input{session} |
37 |
43 |