nominal2: Quotient-Paper/document/root.tex@b52e8651591f (annotated)

2415 e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	\documentclass{sig-alternate}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	2	\pdfpagewidth=8.5truein
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	\pdfpageheight=11truein
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4	\usepackage{times}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	\usepackage{isabelle}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6	\usepackage{isabellesym}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7	\usepackage{amsmath}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	8	\usepackage{amssymb}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	9	\usepackage{pdfsetup}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	10	\usepackage{tikz}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	11	\usepackage{pgf}
2444 d769c24094cf made all typographic changes Christian Urban <urbanc@in.tum.de> parents: 2443 diff changeset	12	\usepackage{stmaryrd}
2415 e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	13	\usepackage{verbdef}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	14	\usepackage{longtable}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	\usepackage{mathpartir}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16	\newtheorem{definition}{Definition}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	\newtheorem{proposition}{Proposition}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	\newtheorem{lemma}{Lemma}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20	\urlstyle{rm}
2443 5606de1e5034 first pass on section 1 Christian Urban <urbanc@in.tum.de> parents: 2442 diff changeset	21	\isabellestyle{rm}
5606de1e5034 first pass on section 1 Christian Urban <urbanc@in.tum.de> parents: 2442 diff changeset	22	\renewcommand{\isastyleminor}{\rm}%
2415 e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	23	\renewcommand{\isastyle}{\normalsize\rm}%
2444 d769c24094cf made all typographic changes Christian Urban <urbanc@in.tum.de> parents: 2443 diff changeset	24	\renewcommand{\isastylescript}{\it}
d769c24094cf made all typographic changes Christian Urban <urbanc@in.tum.de> parents: 2443 diff changeset	25	\def\dn{\,\triangleq\,}
d769c24094cf made all typographic changes Christian Urban <urbanc@in.tum.de> parents: 2443 diff changeset	26	\verbdef\singlearr\|---->\|
2415 e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	27	\verbdef\doublearr\|===>\|
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	28	\verbdef\tripple\|###\|
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	29
2443 5606de1e5034 first pass on section 1 Christian Urban <urbanc@in.tum.de> parents: 2442 diff changeset	30	\renewcommand{\isasymequiv}{$\triangleq$}
2415 e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31	\renewcommand{\isasymemptyset}{$\varnothing$}
2443 5606de1e5034 first pass on section 1 Christian Urban <urbanc@in.tum.de> parents: 2442 diff changeset	32	%%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
2415 e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	33	\renewcommand{\isasymUnion}{$\bigcup$}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	34
2444 d769c24094cf made all typographic changes Christian Urban <urbanc@in.tum.de> parents: 2443 diff changeset	35	\newcommand{\isasymsinglearr}{$\mapsto$}
d769c24094cf made all typographic changes Christian Urban <urbanc@in.tum.de> parents: 2443 diff changeset	36	\newcommand{\isasymdoublearr}{$\Mapsto$}
2415 e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	37	\newcommand{\isasymtripple}{\tripple}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	38
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	39	\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	40
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	41	\begin{document}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	42
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	43	\conferenceinfo{SAC'11}{March 21-25, 2011, TaiChung, Taiwan.}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	44	\CopyrightYear{2011}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	45	\crdata{978-1-4503-0113-8/11/03}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	46
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	47	\title{Quotients Revisited for Isabelle/HOL}
2552 bf4b28ebb412 Unanonymize qpaper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2527 diff changeset	48	\numberofauthors{2}
bf4b28ebb412 Unanonymize qpaper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2527 diff changeset	49	\author{
bf4b28ebb412 Unanonymize qpaper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2527 diff changeset	50	\alignauthor
bf4b28ebb412 Unanonymize qpaper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2527 diff changeset	51	Cezary Kaliszyk\\
bf4b28ebb412 Unanonymize qpaper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2527 diff changeset	52	\affaddr{University of Tsukuba, Japan}\\
bf4b28ebb412 Unanonymize qpaper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2527 diff changeset	53	\email{kaliszyk@cs.tsukuba.ac.jp}
bf4b28ebb412 Unanonymize qpaper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2527 diff changeset	54	\alignauthor
bf4b28ebb412 Unanonymize qpaper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2527 diff changeset	55	Christian Urban\\
bf4b28ebb412 Unanonymize qpaper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2527 diff changeset	56	\affaddr{Technical University of Munich, Germany}\\
bf4b28ebb412 Unanonymize qpaper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2527 diff changeset	57	\email{urbanc@in.tum.de}
bf4b28ebb412 Unanonymize qpaper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2527 diff changeset	58	}
2415 e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	59
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	60	\maketitle
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	61
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	62	\begin{abstract}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	63	Higher-Order Logic (HOL) is based on a small logic kernel, whose only
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	64	mechanism for extension is the introduction of safe definitions and of
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	65	non-empty types. Both extensions are often performed in quotient
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	66	constructions. To ease the work involved with such quotient constructions, we
2554 2668486b684a squeezed qpaper to 6 pages Christian Urban <urbanc@in.tum.de> parents: 2552 diff changeset	67	re-implemented in the %popular
2668486b684a squeezed qpaper to 6 pages Christian Urban <urbanc@in.tum.de> parents: 2552 diff changeset	68	Isabelle/HOL theorem prover the quotient
2443 5606de1e5034 first pass on section 1 Christian Urban <urbanc@in.tum.de> parents: 2442 diff changeset	69	package by Homeier. In doing so we extended his work in order to deal with
2445 10148a447359 cut out most of the lifting section and cleaned up everything Christian Urban <urbanc@in.tum.de> parents: 2444 diff changeset	70	compositions of quotients and also specified completely the procedure
2443 5606de1e5034 first pass on section 1 Christian Urban <urbanc@in.tum.de> parents: 2442 diff changeset	71	of lifting theorems from the raw level to the quotient level.
5606de1e5034 first pass on section 1 Christian Urban <urbanc@in.tum.de> parents: 2442 diff changeset	72	The importance for theorem proving is that many formal
2527 40187684fc16 fixed the typo in the abstract and the problem with append (the type of map_k Christian Urban <urbanc@in.tum.de> parents: 2455 diff changeset	73	verifications, in order to be feasible, require a convenient reasoning infrastructure
2443 5606de1e5034 first pass on section 1 Christian Urban <urbanc@in.tum.de> parents: 2442 diff changeset	74	for quotient constructions.
2415 e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	75	\end{abstract}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	76
2443 5606de1e5034 first pass on section 1 Christian Urban <urbanc@in.tum.de> parents: 2442 diff changeset	77	%\category{D.??}{TODO}{TODO}
2415 e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	78
2443 5606de1e5034 first pass on section 1 Christian Urban <urbanc@in.tum.de> parents: 2442 diff changeset	79	\keywords{Quotients, Isabelle theorem prover, Higher-Order Logic}
2415 e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	80
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	81	% generated text of all theories
2558 6cfb5d8a5b5b expanded the paper by uncommenting the comments and adding the appendix Christian Urban <urbanc@in.tum.de> parents: 2554 diff changeset	82	\bibliographystyle{abbrv}
2415 e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	83	\input{session}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	84
2554 2668486b684a squeezed qpaper to 6 pages Christian Urban <urbanc@in.tum.de> parents: 2552 diff changeset	85
2415 e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	86
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	87	\end{document}
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	88
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	89	%%% Local Variables:
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	90	%%% mode: latex
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	91	%%% TeX-master: t
e96f3efb0032 Add the SAC stylesheet and updated root file. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	92	%%% End:

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Thu, 13 Mar 2014 09:21:31 +0000
changeset 3229	b52e8651591f
parent 2558	6cfb5d8a5b5b
permissions	-rw-r--r--