4 \usepackage{isabelle} |
4 \usepackage{isabelle} |
5 \usepackage{isabellesym} |
5 \usepackage{isabellesym} |
6 \usepackage{amsmath} |
6 \usepackage{amsmath} |
7 \usepackage{amssymb} |
7 \usepackage{amssymb} |
8 \usepackage{pdfsetup} |
8 \usepackage{pdfsetup} |
9 |
9 \usepackage{tikz} |
|
10 \usepackage{pgf} |
|
11 \usepackage{verbdef} |
|
12 \usepackage{longtable} |
|
13 \usepackage{mathpartir} |
10 |
14 |
11 \urlstyle{rm} |
15 \urlstyle{rm} |
12 \isabellestyle{it} |
16 \isabellestyle{it} |
13 \renewcommand{\isastyle}{\isastyleminor} |
17 \renewcommand{\isastyle}{\isastyleminor} |
14 |
18 |
15 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
19 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
|
20 \verbdef\singlearr|--->| |
|
21 \verbdef\doublearr|===>| |
|
22 \verbdef\tripple|###| |
|
23 |
16 \renewcommand{\isasymequiv}{$\dn$} |
24 \renewcommand{\isasymequiv}{$\dn$} |
17 \renewcommand{\isasymemptyset}{$\varnothing$} |
25 \renewcommand{\isasymemptyset}{$\varnothing$} |
|
26 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
|
27 \renewcommand{\isasymUnion}{$\bigcup$} |
|
28 |
|
29 \newcommand{\isasymsinglearr}{\singlearr} |
|
30 \newcommand{\isasymdoublearr}{\doublearr} |
|
31 \newcommand{\isasymtripple}{\tripple} |
|
32 |
|
33 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}} |
18 |
34 |
19 \begin{document} |
35 \begin{document} |
20 |
36 |
21 \title{Quotients Revisited for Isabelle/HOL} |
37 \title{Quotients Revisited for Isabelle/HOL} |
22 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$} |
38 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$} |
23 \institute{$^*$ Technical University of Munich, Germany} |
39 \institute{$^*$ Technical University of Munich, Germany} |
24 \maketitle |
40 \maketitle |
25 |
41 |
26 \begin{abstract} |
42 \begin{abstract} |
27 Higher-order logic (HOL), used in a number of theorem provers, is based on a small |
43 Higher-Order Logic (HOL) is based on a small logic kernel, whose only |
28 logic kernel, whose only mechanism for extension is the introduction of safe |
44 mechanism for extension is the introduction of safe definitions and of |
29 definitions and non-empty types. Both extensions are often performed by |
45 non-empty types. Both extensions are often performed in quotient |
30 quotient constructions; for example finite sets are constructed by quotienting |
46 constructions. To ease the work involved with such quotient constructions, we |
31 lists, or integers by quotienting pairs of natural numbers. To ease the work |
47 re-implemented in Isabelle/HOL the quotient package by Homeier. In doing so we |
32 involved with quotient constructions, we re-implemented in Isabelle/HOL the |
48 extended his work in order to deal with compositions of quotients. We also |
33 quotient package by Homeier. In doing so we extended his work in order to deal |
49 designed our quotient package so that every step in a quotient construction |
34 with compositions of quotients. Also, we designed our quotient package so that |
50 can be performed separately and as a result we are able to specify completely |
35 every step in a quotient construction can be performed separately and as a |
51 the procedure of lifting theorems from the raw level to the quotient level. |
36 result we were able to specify completely the procedure of lifting theorems from |
52 The importance for programming language research is that many properties of |
37 the raw level to the quotient level. The importance to programming language |
53 programming language calculi are easier to verify over $\alpha$-equated, or |
38 research is that many properties of programming languages are more convenient |
54 $\alpha$-quotient, terms, than over raw terms. |
39 to verify over $\alpha$-quotient terms, than over raw terms. |
|
40 \end{abstract} |
55 \end{abstract} |
41 |
56 |
42 % generated text of all theories |
57 % generated text of all theories |
43 \input{session} |
58 \input{session} |
44 |
59 |