\documentclass{sig-alternate}+ −
\pdfpagewidth=8.5truein+ −
\pdfpageheight=11truein+ −
\usepackage{times}+ −
\usepackage{isabelle}+ −
\usepackage{isabellesym}+ −
\usepackage{amsmath}+ −
\usepackage{amssymb}+ −
\usepackage{pdfsetup}+ −
\usepackage{tikz}+ −
\usepackage{pgf}+ −
\usepackage{stmaryrd}+ −
\usepackage{verbdef}+ −
\usepackage{longtable}+ −
\usepackage{mathpartir}+ −
\newtheorem{definition}{Definition}+ −
\newtheorem{proposition}{Proposition}+ −
\newtheorem{lemma}{Lemma}+ −
+ −
\urlstyle{rm}+ −
\isabellestyle{rm}+ −
\renewcommand{\isastyleminor}{\rm}%+ −
\renewcommand{\isastyle}{\normalsize\rm}%+ −
\renewcommand{\isastylescript}{\it}+ −
\def\dn{\,\triangleq\,}+ −
\verbdef\singlearr|---->|+ −
\verbdef\doublearr|===>|+ −
\verbdef\tripple|###|+ −
+ −
\renewcommand{\isasymequiv}{$\triangleq$}+ −
\renewcommand{\isasymemptyset}{$\varnothing$}+ −
%%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}+ −
\renewcommand{\isasymUnion}{$\bigcup$}+ −
+ −
\newcommand{\isasymsinglearr}{$\mapsto$}+ −
\newcommand{\isasymdoublearr}{$\Mapsto$}+ −
\newcommand{\isasymtripple}{\tripple}+ −
+ −
\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}+ −
+ −
\begin{document}+ −
+ −
\conferenceinfo{SAC'11}{March 21-25, 2011, TaiChung, Taiwan.}+ −
\CopyrightYear{2011}+ −
\crdata{978-1-4503-0113-8/11/03}+ −
+ −
\title{Quotients Revisited for Isabelle/HOL}+ −
\numberofauthors{2}+ −
\author{+ −
\alignauthor+ −
Cezary Kaliszyk\\+ −
\affaddr{University of Tsukuba, Japan}\\+ −
\email{kaliszyk@cs.tsukuba.ac.jp}+ −
\alignauthor+ −
Christian Urban\\+ −
\affaddr{Technical University of Munich, Germany}\\+ −
\email{urbanc@in.tum.de}+ −
}+ −
+ −
\maketitle+ −
+ −
\begin{abstract}+ −
Higher-Order Logic (HOL) is based on a small logic kernel, whose only+ −
mechanism for extension is the introduction of safe definitions and of+ −
non-empty types. Both extensions are often performed in quotient+ −
constructions. To ease the work involved with such quotient constructions, we+ −
re-implemented in the popular Isabelle/HOL theorem prover the quotient + −
package by Homeier. In doing so we extended his work in order to deal with + −
compositions of quotients and also specified completely the procedure + −
of lifting theorems from the raw level to the quotient level.+ −
The importance for theorem proving is that many formal+ −
verifications, in order to be feasible, require a convenient reasoning infrastructure + −
for quotient constructions.+ −
\end{abstract}+ −
+ −
%\category{D.??}{TODO}{TODO}+ −
+ −
\keywords{Quotients, Isabelle theorem prover, Higher-Order Logic}+ −
+ −
% generated text of all theories+ −
\input{session}+ −
+ −
% optional bibliography+ −
\bibliographystyle{abbrv}+ −
\bibliography{root}+ −
+ −
\end{document}+ −
+ −
%%% Local Variables:+ −
%%% mode: latex+ −
%%% TeX-master: t+ −
%%% End:+ −