|
1 \documentclass{svjour3} |
|
2 \usepackage{times} |
|
3 \usepackage{isabelle} |
|
4 \usepackage{isabellesym} |
|
5 \usepackage{amsmath} |
|
6 \usepackage{amssymb} |
|
7 \usepackage{pdfsetup} |
|
8 \usepackage{tikz} |
|
9 %\usepackage{pgf} |
|
10 \usepackage{stmaryrd} |
|
11 \usepackage{verbdef} |
|
12 %\usepackage{longtable} |
|
13 \usepackage{mathpartir} |
|
14 %\newtheorem{definition}{Definition} |
|
15 %\newtheorem{proposition}{Proposition} |
|
16 %\newtheorem{lemma}{Lemma} |
|
17 |
|
18 \urlstyle{rm} |
|
19 \isabellestyle{rm} |
|
20 \renewcommand{\isastyleminor}{\rm}% |
|
21 \renewcommand{\isastyle}{\normalsize\rm}% |
|
22 \renewcommand{\isastylescript}{\it} |
|
23 \def\dn{\,\triangleq\,} |
|
24 \verbdef\singlearr|---->| |
|
25 \verbdef\doublearr|===>| |
|
26 \verbdef\tripple|###| |
|
27 |
|
28 \renewcommand{\isasymequiv}{$\triangleq$} |
|
29 \renewcommand{\isasymemptyset}{$\varnothing$} |
|
30 %%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
|
31 \renewcommand{\isasymUnion}{$\bigcup$} |
|
32 |
|
33 \newcommand{\isasymsinglearr}{$\mapsto$} |
|
34 \newcommand{\isasymdoublearr}{$\Mapsto$} |
|
35 \newcommand{\isasymtripple}{\tripple} |
|
36 |
|
37 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}} |
|
38 |
|
39 \begin{document} |
|
40 |
|
41 \title{Quotients Revisited for Isabelle/HOL} |
|
42 \author{Cezary Kaliszyk \and Christian Urban} |
|
43 \institute{C.~Kaliszyk \at University of Tsukuba, Japan |
|
44 \and C.~Urban \at Technical University of Munich, Germany} |
|
45 \date{Received: date / Accepted: date} |
|
46 |
|
47 \maketitle |
|
48 |
|
49 \begin{abstract} |
|
50 Higher-Order Logic (HOL) is based on a small logic kernel, whose only |
|
51 mechanism for extension is the introduction of safe definitions and of |
|
52 non-empty types. Both extensions are often performed in quotient |
|
53 constructions. To ease the work involved with such quotient constructions, we |
|
54 re-implemented in the %popular |
|
55 Isabelle/HOL theorem prover the quotient |
|
56 package by Homeier. In doing so we extended his work in order to deal with |
|
57 compositions of quotients and also specified completely the procedure |
|
58 of lifting theorems from the raw level to the quotient level. |
|
59 The importance for theorem proving is that many formal |
|
60 verifications, in order to be feasible, require a convenient reasoning infrastructure |
|
61 for quotient constructions. |
|
62 \end{abstract} |
|
63 |
|
64 %\keywords{Quotients, Isabelle theorem prover, Higher-Order Logic} |
|
65 |
|
66 \bibliographystyle{abbrv} |
|
67 \input{session} |
|
68 |
|
69 |
|
70 |
|
71 \end{document} |
|
72 |
|
73 %%% Local Variables: |
|
74 %%% mode: latex |
|
75 %%% TeX-master: t |
|
76 %%% End: |