15 \newtheorem{definition}{Definition} |
15 \newtheorem{definition}{Definition} |
16 \newtheorem{proposition}{Proposition} |
16 \newtheorem{proposition}{Proposition} |
17 \newtheorem{lemma}{Lemma} |
17 \newtheorem{lemma}{Lemma} |
18 |
18 |
19 \urlstyle{rm} |
19 \urlstyle{rm} |
20 \isabellestyle{it} |
20 \isabellestyle{rm} |
21 \renewcommand{\isastyleminor}{\it}% |
21 \renewcommand{\isastyleminor}{\rm}% |
22 \renewcommand{\isastyle}{\normalsize\rm}% |
22 \renewcommand{\isastyle}{\normalsize\rm}% |
23 |
23 |
24 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
24 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
25 \verbdef\singlearr|--->| |
25 \verbdef\singlearr|--->| |
26 \verbdef\doublearr|===>| |
26 \verbdef\doublearr|===>| |
27 \verbdef\tripple|###| |
27 \verbdef\tripple|###| |
28 |
28 |
29 \renewcommand{\isasymequiv}{$\dn$} |
29 \renewcommand{\isasymequiv}{$\triangleq$} |
30 \renewcommand{\isasymemptyset}{$\varnothing$} |
30 \renewcommand{\isasymemptyset}{$\varnothing$} |
31 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
31 %%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
32 \renewcommand{\isasymUnion}{$\bigcup$} |
32 \renewcommand{\isasymUnion}{$\bigcup$} |
33 |
33 |
34 \newcommand{\isasymsinglearr}{\singlearr} |
34 \newcommand{\isasymsinglearr}{\singlearr} |
35 \newcommand{\isasymdoublearr}{\doublearr} |
35 \newcommand{\isasymdoublearr}{\doublearr} |
36 \newcommand{\isasymtripple}{\tripple} |
36 \newcommand{\isasymtripple}{\tripple} |
61 \begin{abstract} |
61 \begin{abstract} |
62 Higher-Order Logic (HOL) is based on a small logic kernel, whose only |
62 Higher-Order Logic (HOL) is based on a small logic kernel, whose only |
63 mechanism for extension is the introduction of safe definitions and of |
63 mechanism for extension is the introduction of safe definitions and of |
64 non-empty types. Both extensions are often performed in quotient |
64 non-empty types. Both extensions are often performed in quotient |
65 constructions. To ease the work involved with such quotient constructions, we |
65 constructions. To ease the work involved with such quotient constructions, we |
66 re-implemented in Isabelle/HOL the quotient package by Homeier. In doing so we |
66 re-implemented in the popular Isabelle/HOL theorem prover the quotient |
67 extended his work in order to deal with compositions of quotients. Like his |
67 package by Homeier. In doing so we extended his work in order to deal with |
68 package, we designed our quotient package so that every step in a quotient construction |
68 compositions of quotients and we are also able to specify completely the procedure |
69 can be performed separately and as a result we are able to specify completely |
69 of lifting theorems from the raw level to the quotient level. |
70 the procedure of lifting theorems from the raw level to the quotient level. |
70 The importance for theorem proving is that many formal |
71 The importance for programming language research is that many properties of |
71 verifications, in order to be feasible, require a convenient resoning infrastructure |
72 programming language calculi are easier to verify over $\alpha$-equated, or |
72 for quotient constructions. |
73 $\alpha$-quotient, terms, than over raw terms. |
|
74 \end{abstract} |
73 \end{abstract} |
75 |
74 |
76 \category{D.??}{TODO}{TODO} |
75 %\category{D.??}{TODO}{TODO} |
77 |
76 |
78 \keywords{quotients, isabelle, higher order logic} |
77 \keywords{Quotients, Isabelle theorem prover, Higher-Order Logic} |
79 |
78 |
80 % generated text of all theories |
79 % generated text of all theories |
81 \input{session} |
80 \input{session} |
82 |
81 |
83 % optional bibliography |
82 % optional bibliography |