1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 1
(*<*)
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 2
theory Paper
2183
+ − 3
imports "Quotient"
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 4
"LaTeXsugar"
2186
+ − 5
"../Nominal/FSet"
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 6
begin
1994
+ − 7
2286
e7bc2ae30faf
added a few points that need to be looked at the next version of the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 8
(****
e7bc2ae30faf
added a few points that need to be looked at the next version of the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 9
e7bc2ae30faf
added a few points that need to be looked at the next version of the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 10
** things to do for the next version
e7bc2ae30faf
added a few points that need to be looked at the next version of the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 11
*
e7bc2ae30faf
added a few points that need to be looked at the next version of the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 12
* - what are quot_thms?
2287
+ − 13
* - what do all preservation theorems look like,
+ − 14
in particular preservation for quotient
+ − 15
compositions
2333
+ − 16
- explain how Quotient R Abs Rep is proved (j-version)
+ − 17
- give an example where precise specification helps (core Haskell in nominal?)
2286
e7bc2ae30faf
added a few points that need to be looked at the next version of the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 18
*)
e7bc2ae30faf
added a few points that need to be looked at the next version of the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 19
1994
+ − 20
notation (latex output)
2258
+ − 21
rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
2269
+ − 22
pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
2258
+ − 23
"op -->" (infix "\<longrightarrow>" 100) and
+ − 24
"==>" (infix "\<Longrightarrow>" 100) and
2227
+ − 25
fun_map ("_ \<^raw:\mbox{\singlearr}> _" 51) and
+ − 26
fun_rel ("_ \<^raw:\mbox{\doublearr}> _" 51) and
2217
+ − 27
list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
2223
+ − 28
fempty ("\<emptyset>") and
+ − 29
funion ("_ \<union> _") and
+ − 30
finsert ("{_} \<union> _") and
2221
+ − 31
Cons ("_::_") and
+ − 32
concat ("flat") and
2223
+ − 33
fconcat ("\<Union>")
2220
+ − 34
2217
+ − 35
1994
+ − 36
2182
+ − 37
ML {*
+ − 38
fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;
2274
+ − 39
2182
+ − 40
fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
+ − 41
let
+ − 42
val concl =
+ − 43
Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)
+ − 44
in
+ − 45
case concl of (_ $ l $ r) => proj (l, r)
+ − 46
| _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
+ − 47
end);
+ − 48
*}
2274
+ − 49
2182
+ − 50
setup {*
+ − 51
Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #>
+ − 52
Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #>
+ − 53
Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))
+ − 54
*}
2274
+ − 55
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 56
(*>*)
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 57
2227
+ − 58
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 59
section {* Introduction *}
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 60
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 61
text {*
2205
+ − 62
\begin{flushright}
+ − 63
{\em ``Not using a [quotient] package has its advantages: we do not have to\\
+ − 64
collect all the theorems we shall ever want into one giant list;''}\\
2213
+ − 65
Larry Paulson \cite{Paulson06}
2237
+ − 66
\end{flushright}
2103
+ − 67
+ − 68
\noindent
2220
+ − 69
Isabelle is a popular generic theorem prover in which many logics can be
2214
+ − 70
implemented. The most widely used one, however, is Higher-Order Logic
+ − 71
(HOL). This logic consists of a small number of axioms and inference rules
+ − 72
over a simply-typed term-language. Safe reasoning in HOL is ensured by two
+ − 73
very restricted mechanisms for extending the logic: one is the definition of
+ − 74
new constants in terms of existing ones; the other is the introduction of
+ − 75
new types by identifying non-empty subsets in existing types. It is well
2223
+ − 76
understood how to use both mechanisms for dealing with quotient
2220
+ − 77
constructions in HOL (see \cite{Homeier05,Paulson06}). For example the
+ − 78
integers in Isabelle/HOL are constructed by a quotient construction over the
+ − 79
type @{typ "nat \<times> nat"} and the equivalence relation
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 80
2237
+ − 81
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ − 82
@{text "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + m\<^isub>2 = m\<^isub>1 + n\<^isub>2"}\hfill\numbered{natpairequiv}
+ − 83
\end{isabelle}
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 84
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 85
\noindent
2217
+ − 86
This constructions yields the new type @{typ int} and definitions for @{text
2220
+ − 87
"0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of
+ − 88
natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations
+ − 89
such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in
+ − 90
terms of operations on pairs of natural numbers (namely @{text
2224
+ − 91
"add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2,
2222
+ − 92
m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}).
+ − 93
Similarly one can construct the type of finite sets, written @{term "\<alpha> fset"},
2223
+ − 94
by quotienting the type @{text "\<alpha> list"} according to the equivalence relation
2103
+ − 95
2237
+ − 96
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ − 97
@{text "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}\hfill\numbered{listequiv}
+ − 98
\end{isabelle}
2103
+ − 99
+ − 100
\noindent
2224
+ − 101
which states that two lists are equivalent if every element in one list is
+ − 102
also member in the other. The empty finite set, written @{term "{||}"}, can
+ − 103
then be defined as the empty list and the union of two finite sets, written
+ − 104
@{text "\<union>"}, as list append.
2220
+ − 105
2269
+ − 106
Quotients are important in a variety of areas, but they are really ubiquitous in
2258
+ − 107
the area of reasoning about programming language calculi. A simple example
+ − 108
is the lambda-calculus, whose raw terms are defined as
+ − 109
2220
+ − 110
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 111
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 112
@{text "t ::= x | t t | \<lambda>x.t"}\hfill\numbered{lambda}
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 113
\end{isabelle}
2217
+ − 114
2220
+ − 115
\noindent
2256
+ − 116
The problem with this definition arises, for instance, when one attempts to
+ − 117
prove formally the substitution lemma \cite{Barendregt81} by induction
2222
+ − 118
over the structure of terms. This can be fiendishly complicated (see
2220
+ − 119
\cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof
2226
+ − 120
about raw lambda-terms). In contrast, if we reason about
2220
+ − 121
$\alpha$-equated lambda-terms, that means terms quotient according to
2223
+ − 122
$\alpha$-equivalence, then the reasoning infrastructure provided,
+ − 123
for example, by Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal
2222
+ − 124
proof of the substitution lemma almost trivial.
2220
+ − 125
+ − 126
The difficulty is that in order to be able to reason about integers, finite
2221
+ − 127
sets or $\alpha$-equated lambda-terms one needs to establish a reasoning
2220
+ − 128
infrastructure by transferring, or \emph{lifting}, definitions and theorems
2226
+ − 129
from the raw type @{typ "nat \<times> nat"} to the quotient type @{typ int}
2220
+ − 130
(similarly for finite sets and $\alpha$-equated lambda-terms). This lifting
2222
+ − 131
usually requires a \emph{lot} of tedious reasoning effort \cite{Paulson06}.
2252
+ − 132
It is feasible to do this work manually, if one has only a few quotient
2247
+ − 133
constructions at hand. But if they have to be done over and over again, as in
2222
+ − 134
Nominal Isabelle, then manual reasoning is not an option.
2221
+ − 135
2223
+ − 136
The purpose of a \emph{quotient package} is to ease the lifting of theorems
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 137
and automate the reasoning as much as possible. In the
2223
+ − 138
context of HOL, there have been a few quotient packages already
2234
+ − 139
\cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier
2223
+ − 140
\cite{Homeier05} implemented in HOL4. The fundamental construction these
+ − 141
quotient packages perform can be illustrated by the following picture:
2217
+ − 142
+ − 143
\begin{center}
2220
+ − 144
\mbox{}\hspace{20mm}\begin{tikzpicture}
+ − 145
%%\draw[step=2mm] (-4,-1) grid (4,1);
+ − 146
+ − 147
\draw[very thick] (0.7,0.3) circle (4.85mm);
+ − 148
\draw[rounded corners=1mm, very thick] ( 0.0,-0.9) rectangle ( 1.8, 0.9);
+ − 149
\draw[rounded corners=1mm, very thick] (-1.95,0.8) rectangle (-2.9,-0.195);
+ − 150
+ − 151
\draw (-2.0, 0.8) -- (0.7,0.8);
+ − 152
\draw (-2.0,-0.195) -- (0.7,-0.195);
2103
+ − 153
2220
+ − 154
\draw ( 0.7, 0.23) node {\begin{tabular}{@ {}c@ {}}equiv-\\[-1mm]clas.\end{tabular}};
+ − 155
\draw (-2.45, 0.35) node {\begin{tabular}{@ {}c@ {}}new\\[-1mm]type\end{tabular}};
+ − 156
\draw (1.8, 0.35) node[right=-0.1mm]
2224
+ − 157
{\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw elements)\end{tabular}};
2220
+ − 158
\draw (0.9, -0.55) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
+ − 159
+ − 160
\draw[->, very thick] (-1.8, 0.36) -- (-0.1,0.36);
+ − 161
\draw[<-, very thick] (-1.8, 0.16) -- (-0.1,0.16);
2221
+ − 162
\draw (-0.95, 0.26) node[above=0.4mm] {@{text Rep}};
+ − 163
\draw (-0.95, 0.26) node[below=0.4mm] {@{text Abs}};
2220
+ − 164
+ − 165
\end{tikzpicture}
+ − 166
\end{center}
2217
+ − 167
2221
+ − 168
\noindent
2247
+ − 169
The starting point is an existing type, to which we refer as the
2269
+ − 170
\emph{raw type} and over which an equivalence relation given by the user is
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 171
defined. With this input the package introduces a new type, to which we
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 172
refer as the \emph{quotient type}. This type comes with an
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 173
\emph{abstraction} and a \emph{representation} function, written @{text Abs}
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 174
and @{text Rep}.\footnote{Actually slightly more basic functions are given;
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 175
the functions @{text Abs} and @{text Rep} need to be derived from them. We
2269
+ − 176
will show the details later. } They relate elements in the
+ − 177
existing type to elements in the new type and vice versa, and can be uniquely
2256
+ − 178
identified by their quotient type. For example for the integer quotient construction
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 179
the types of @{text Abs} and @{text Rep} are
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 180
2224
+ − 181
+ − 182
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
2234
+ − 183
@{text "Abs :: nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep :: int \<Rightarrow> nat \<times> nat"}
2224
+ − 184
\end{isabelle}
+ − 185
+ − 186
\noindent
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 187
We therefore often write @{text Abs_int} and @{text Rep_int} if the
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 188
typing information is important.
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 189
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 190
Every abstraction and representation function stands for an isomorphism
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 191
between the non-empty subset and elements in the new type. They are
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 192
necessary for making definitions involving the new type. For example @{text
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 193
"0"} and @{text "1"} of type @{typ int} can be defined as
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 194
2221
+ − 195
+ − 196
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 197
@{text "0 \<equiv> Abs_int (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs_int (1, 0)"}
2221
+ − 198
\end{isabelle}
+ − 199
+ − 200
\noindent
2224
+ − 201
Slightly more complicated is the definition of @{text "add"} having type
2222
+ − 202
@{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition is as follows
2221
+ − 203
2258
+ − 204
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ − 205
@{text "add n m \<equiv> Abs_int (add_pair (Rep_int n) (Rep_int m))"}
+ − 206
\hfill\numbered{adddef}
+ − 207
\end{isabelle}
+ − 208
2221
+ − 209
\noindent
2224
+ − 210
where we take the representation of the arguments @{text n} and @{text m},
2226
+ − 211
add them according to the function @{text "add_pair"} and then take the
2221
+ − 212
abstraction of the result. This is all straightforward and the existing
+ − 213
quotient packages can deal with such definitions. But what is surprising
2223
+ − 214
that none of them can deal with slightly more complicated definitions involving
2221
+ − 215
\emph{compositions} of quotients. Such compositions are needed for example
2247
+ − 216
in case of quotienting lists to yield finite sets and the operator that
2226
+ − 217
flattens lists of lists, defined as follows
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 218
2220
+ − 219
@{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]}
2183
+ − 220
2103
+ − 221
\noindent
2221
+ − 222
We expect that the corresponding operator on finite sets, written @{term "fconcat"},
2248
+ − 223
builds finite unions of finite sets:
2188
+ − 224
2220
+ − 225
@{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 226
2103
+ − 227
\noindent
2256
+ − 228
The quotient package should automatically provide us with a definition for @{text "\<Union>"} in
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 229
terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 230
that the method used in the existing quotient
2247
+ − 231
packages of just taking the representation of the arguments and then taking
2258
+ − 232
the abstraction of the result is \emph{not} enough. The reason is that in case
2224
+ − 233
of @{text "\<Union>"} we obtain the incorrect definition
+ − 234
2234
+ − 235
@{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}
2221
+ − 236
2224
+ − 237
\noindent
+ − 238
where the right-hand side is not even typable! This problem can be remedied in the
+ − 239
existing quotient packages by introducing an intermediate step and reasoning
2226
+ − 240
about flattening of lists of finite sets. However, this remedy is rather
2224
+ − 241
cumbersome and inelegant in light of our work, which can deal with such
+ − 242
definitions directly. The solution is that we need to build aggregate
+ − 243
representation and abstraction functions, which in case of @{text "\<Union>"}
+ − 244
generate the following definition
+ − 245
2234
+ − 246
@{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat ((map Rep_fset \<circ> Rep_fset) S))"}
2221
+ − 247
+ − 248
\noindent
2223
+ − 249
where @{term map} is the usual mapping function for lists. In this paper we
2224
+ − 250
will present a formal definition of our aggregate abstraction and
2223
+ − 251
representation functions (this definition was omitted in \cite{Homeier05}).
2224
+ − 252
They generate definitions, like the one above for @{text "\<Union>"},
2226
+ − 253
according to the type of the raw constant and the type
2224
+ − 254
of the quotient constant. This means we also have to extend the notions
2237
+ − 255
of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}
2231
+ − 256
from Homeier \cite{Homeier05}.
2223
+ − 257
2252
+ − 258
In addition we are able to address the criticism by Paulson \cite{Paulson06} cited
2237
+ − 259
at the beginning of this section about having to collect theorems that are
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 260
lifted from the raw level to the quotient level into one giant list. Homeier's and
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 261
also our quotient package are modular so that they allow lifting
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 262
theorems separately. This has the advantage for the user of being able to develop a
2252
+ − 263
formal theory interactively as a natural progression. A pleasing side-result of
2256
+ − 264
the modularity is that we are able to clearly specify what is involved
+ − 265
in the lifting process (this was only hinted at in \cite{Homeier05} and
2247
+ − 266
implemented as a ``rough recipe'' in ML-code).
+ − 267
2237
+ − 268
+ − 269
The paper is organised as follows: Section \ref{sec:prelims} presents briefly
2247
+ − 270
some necessary preliminaries; Section \ref{sec:type} describes the definitions
2252
+ − 271
of quotient types and shows how definitions of constants can be made over
2277
+ − 272
quotient types. Section \ref{sec:resp} introduces the notions of respectfulness
2274
+ − 273
and preservation; Section \ref{sec:lift} describes the lifting of theorems;
+ − 274
Section \ref{sec:examples} presents some examples
2256
+ − 275
and Section \ref{sec:conc} concludes and compares our results to existing
+ − 276
work.
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 277
*}
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 278
2257
+ − 279
section {* Preliminaries and General Quotients\label{sec:prelims} *}
1978
+ − 280
+ − 281
text {*
2274
+ − 282
We give in this section a crude overview of HOL and describe the main
+ − 283
definitions given by Homeier for quotients \cite{Homeier05}.
2258
+ − 284
2274
+ − 285
At its core, HOL is based on a simply-typed term language, where types are
2269
+ − 286
recorded in Church-style fashion (that means, we can always infer the type of
2258
+ − 287
a term and its subterms without any additional information). The grammars
+ − 288
for types and terms are as follows
2256
+ − 289
+ − 290
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ − 291
\begin{tabular}{@ {}rl@ {\hspace{3mm}}l@ {}}
+ − 292
@{text "\<sigma>, \<tau> ::="} & @{text "\<alpha> | (\<sigma>,\<dots>, \<sigma>) \<kappa>"} & (type variables and type constructors)\\
+ − 293
@{text "t, s ::="} & @{text "x\<^isup>\<sigma> | c\<^isup>\<sigma> | t t | \<lambda>x\<^isup>\<sigma>. t"} &
+ − 294
(variables, constants, applications and abstractions)\\
+ − 295
\end{tabular}
+ − 296
\end{isabelle}
+ − 297
+ − 298
\noindent
+ − 299
We often write just @{text \<kappa>} for @{text "() \<kappa>"}, and use @{text "\<alpha>s"} and
2258
+ − 300
@{text "\<sigma>s"} to stand for collections of type variables and types,
+ − 301
respectively. The type of a term is often made explicit by writing @{text
2274
+ − 302
"t :: \<sigma>"}. HOL includes a type @{typ bool} for booleans and the function
+ − 303
type, written @{text "\<sigma> \<Rightarrow> \<tau>"}. HOL also contains many primitive and defined
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 304
constants; for example, a primitive constant is equality, with type @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
2287
+ − 305
bool"}, and the identity function with type @{text "id :: \<sigma> \<Rightarrow> \<sigma>"} is
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 306
defined as @{text "\<lambda>x\<^sup>\<sigma>. x\<^sup>\<sigma>"}.
2256
+ − 307
2258
+ − 308
An important point to note is that theorems in HOL can be seen as a subset
2287
+ − 309
of terms that are constructed specially (namely through axioms and proof
2269
+ − 310
rules). As a result we are able to define automatic proof
2258
+ − 311
procedures showing that one theorem implies another by decomposing the term
+ − 312
underlying the first theorem.
+ − 313
2333
+ − 314
Like Homeier's, our work relies on map-functions defined for every type
2274
+ − 315
constructor taking some arguments, for example @{text map} for lists. Homeier
+ − 316
describes in \cite{Homeier05} map-functions for products, sums, options and
+ − 317
also the following map for function types
2258
+ − 318
+ − 319
@{thm [display, indent=10] fun_map_def[no_vars, THEN eq_reflection]}
+ − 320
+ − 321
\noindent
+ − 322
Using this map-function, we can give the following, equivalent, but more
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 323
uniform definition for @{text add} shown in \eqref{adddef}:
2256
+ − 324
2258
+ − 325
@{text [display, indent=10] "add \<equiv> (Rep_int \<singlearr> Rep_int \<singlearr> Abs_int) add_pair"}
2182
+ − 326
2258
+ − 327
\noindent
2274
+ − 328
Using extensionality and unfolding the definition of @{text "\<singlearr>"},
+ − 329
we can get back to \eqref{adddef}.
+ − 330
In what follows we shall use the convention to write @{text "map_\<kappa>"} for a map-function
+ − 331
of the type-constructor @{text \<kappa>}. In our implementation we maintain
+ − 332
a database of these map-functions that can be dynamically extended.
2258
+ − 333
+ − 334
It will also be necessary to have operators, referred to as @{text "rel_\<kappa>"},
+ − 335
which define equivalence relations in terms of constituent equivalence
+ − 336
relations. For example given two equivalence relations @{text "R\<^isub>1"}
+ − 337
and @{text "R\<^isub>2"}, we can define an equivalence relations over
+ − 338
products as follows
+ − 339
%
+ − 340
@{text [display, indent=10] "(R\<^isub>1 \<tripple> R\<^isub>2) (x\<^isub>1, x\<^isub>2) (y\<^isub>1, y\<^isub>2) \<equiv> R\<^isub>1 x\<^isub>1 y\<^isub>1 \<and> R\<^isub>2 x\<^isub>2 y\<^isub>2"}
1978
+ − 341
2258
+ − 342
\noindent
2269
+ − 343
Homeier gives also the following operator for defining equivalence
+ − 344
relations over function types
2258
+ − 345
%
2274
+ − 346
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ − 347
@{thm fun_rel_def[of "R\<^isub>1" "R\<^isub>2", no_vars, THEN eq_reflection]}
+ − 348
\hfill\numbered{relfun}
+ − 349
\end{isabelle}
+ − 350
+ − 351
\noindent
2319
+ − 352
In the context of quotients, the following two notions from \cite{Homeier05}
+ − 353
are needed later on.
2274
+ − 354
+ − 355
\begin{definition}[Respects]\label{def:respects}
+ − 356
An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}.
+ − 357
\end{definition}
+ − 358
+ − 359
\begin{definition}[Bounded Quantification and Bounded Abstractions]\label{def:babs}
+ − 360
@{text "\<forall>x \<in> S. P x"} holds if for all @{text x}, @{text "x \<in> S"} implies @{text "P x"};
+ − 361
and @{text "(\<lambda>x \<in> S. f x) = f x"} provided @{text "x \<in> S"}.
+ − 362
\end{definition}
2258
+ − 363
+ − 364
The central definition in Homeier's work \cite{Homeier05} relates equivalence
+ − 365
relations, abstraction and representation functions:
+ − 366
+ − 367
\begin{definition}[Quotient Types]
+ − 368
Given a relation $R$, an abstraction function $Abs$
+ − 369
and a representation function $Rep$, the predicate @{term "Quotient R Abs Rep"}
+ − 370
means
2182
+ − 371
\begin{enumerate}
+ − 372
\item @{thm (rhs1) Quotient_def[of "R", no_vars]}
+ − 373
\item @{thm (rhs2) Quotient_def[of "R", no_vars]}
+ − 374
\item @{thm (rhs3) Quotient_def[of "R", no_vars]}
+ − 375
\end{enumerate}
+ − 376
\end{definition}
+ − 377
2258
+ − 378
\noindent
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 379
The value of this definition lies in the fact that validity of @{text "Quotient R Abs Rep"} can
2269
+ − 380
often be proved in terms of the validity of @{text "Quotient"} over the constituent
+ − 381
types of @{text "R"}, @{text Abs} and @{text Rep}.
2258
+ − 382
For example Homeier proves the following property for higher-order quotient
+ − 383
types:
+ − 384
2269
+ − 385
\begin{proposition}\label{funquot}
2258
+ − 386
@{thm[mode=IfThen] fun_quotient[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"
+ − 387
and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]}
+ − 388
\end{proposition}
2195
+ − 389
2258
+ − 390
\noindent
2274
+ − 391
As a result, Homeier is able to build an automatic prover that can nearly
2269
+ − 392
always discharge a proof obligation involving @{text "Quotient"}. Our quotient
+ − 393
package makes heavy
+ − 394
use of this part of Homeier's work including an extension
2333
+ − 395
for dealing with compositions of equivalence relations defined as follows:
2234
+ − 396
2258
+ − 397
\begin{definition}[Composition of Relations]
+ − 398
@{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate
2319
+ − 399
composition defined by
+ − 400
@{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
2366
+ − 401
holds if and only if there exists a @{text y} such that @{thm (prem 1) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} and
2274
+ − 402
@{thm (prem 2) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}.
2258
+ − 403
\end{definition}
2237
+ − 404
2258
+ − 405
\noindent
2274
+ − 406
Unfortunately, there are two predicaments with compositions of relations.
2366
+ − 407
First, a general quotient theorem for @{text "\<circ>\<circ>\<circ>"}, like the one for @{text "\<singlearr>"}
+ − 408
given in Proposition \ref{funquot},
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 409
cannot be stated inside HOL, because of restrictions on types.
2274
+ − 410
Second, even if we were able to state such a quotient theorem, it
2282
+ − 411
would not be true in general. However, we can prove specific instances of a
+ − 412
quotient theorem for composing particular quotient relations.
2287
+ − 413
For example, to lift theorems involving @{term flat} the quotient theorem for
+ − 414
composing @{text "\<approx>\<^bsub>list\<^esub>"} will be necessary: given @{term "Quotient R Abs Rep"}
+ − 415
with @{text R} being an equivalence relation, then
2282
+ − 416
2319
+ − 417
@{text [display, indent=10] "Quotient (rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (Abs_fset \<circ> map Abs) (map Rep \<circ> Rep_fset)"}
2282
+ − 418
+ − 419
\vspace{-.5mm}
2195
+ − 420
*}
+ − 421
2237
+ − 422
section {* Quotient Types and Quotient Definitions\label{sec:type} *}
1978
+ − 423
2234
+ − 424
text {*
2247
+ − 425
The first step in a quotient construction is to take a name for the new
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 426
type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},
2247
+ − 427
defined over a raw type, say @{text "\<sigma>"}. The type of the equivalence
2269
+ − 428
relation must be @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of
+ − 429
the quotient type declaration is therefore
2234
+ − 430
2235
+ − 431
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
2269
+ − 432
\isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}\hfill\numbered{typedecl}
2235
+ − 433
\end{isabelle}
+ − 434
+ − 435
\noindent
2237
+ − 436
and a proof that @{text "R"} is indeed an equivalence relation. Two concrete
+ − 437
examples are
+ − 438
+ − 439
+ − 440
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ − 441
\begin{tabular}{@ {}l}
+ − 442
\isacommand{quotient\_type}~~@{text "int = nat \<times> nat / \<approx>\<^bsub>nat \<times> nat\<^esub>"}\\
+ − 443
\isacommand{quotient\_type}~~@{text "\<alpha> fset = \<alpha> list / \<approx>\<^bsub>list\<^esub>"}
+ − 444
\end{tabular}
+ − 445
\end{isabelle}
+ − 446
+ − 447
\noindent
+ − 448
which introduce the type of integers and of finite sets using the
+ − 449
equivalence relations @{text "\<approx>\<^bsub>nat \<times> nat\<^esub>"} and @{text
2269
+ − 450
"\<approx>\<^bsub>list\<^esub>"} defined in \eqref{natpairequiv} and
2247
+ − 451
\eqref{listequiv}, respectively (the proofs about being equivalence
2274
+ − 452
relations is omitted). Given this data, we define for declarations shown in
+ − 453
\eqref{typedecl} the quotient types internally as
2234
+ − 454
+ − 455
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ − 456
\isacommand{typedef}~~@{text "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>x. c = R x}"}
+ − 457
\end{isabelle}
+ − 458
+ − 459
\noindent
2247
+ − 460
where the right-hand side is the (non-empty) set of equivalence classes of
2274
+ − 461
@{text "R"}. The constraint in this declaration is that the type variables
2237
+ − 462
in the raw type @{text "\<sigma>"} must be included in the type variables @{text
2274
+ − 463
"\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will then provide us with the following
2269
+ − 464
abstraction and representation functions
2182
+ − 465
2234
+ − 466
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ − 467
@{text "abs_\<kappa>\<^isub>q :: \<sigma> set \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"}\hspace{10mm}@{text "rep_\<kappa>\<^isub>q :: \<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma> set"}
+ − 468
\end{isabelle}
+ − 469
2235
+ − 470
\noindent
2269
+ − 471
As can be seen from the type, they relate the new quotient type and equivalence classes of the raw
2235
+ − 472
type. However, as Homeier \cite{Homeier05} noted, it is much more convenient
+ − 473
to work with the following derived abstraction and representation functions
+ − 474
2234
+ − 475
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ − 476
@{text "Abs_\<kappa>\<^isub>q x \<equiv> abs_\<kappa>\<^isub>q (R x)"}\hspace{10mm}@{text "Rep_\<kappa>\<^isub>q x \<equiv> \<epsilon> (rep_\<kappa>\<^isub>q x)"}
+ − 477
\end{isabelle}
+ − 478
+ − 479
\noindent
2235
+ − 480
on the expense of having to use Hilbert's choice operator @{text "\<epsilon>"} in the
2237
+ − 481
definition of @{text "Rep_\<kappa>\<^isub>q"}. These derived notions relate the
+ − 482
quotient type and the raw type directly, as can be seen from their type,
+ − 483
namely @{text "\<sigma> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"},
+ − 484
respectively. Given that @{text "R"} is an equivalence relation, the
2274
+ − 485
following property holds for every quotient type
+ − 486
(for the proof see \cite{Homeier05}).
2237
+ − 487
2258
+ − 488
\begin{proposition}
2287
+ − 489
@{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.
2258
+ − 490
\end{proposition}
2234
+ − 491
2247
+ − 492
The next step in a quotient construction is to introduce definitions of new constants
+ − 493
involving the quotient type. These definitions need to be given in terms of concepts
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 494
of the raw type (remember this is the only way how to extend HOL
2269
+ − 495
with new definitions). For the user the visible part of such definitions is the declaration
2235
+ − 496
+ − 497
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
2237
+ − 498
\isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~~\isacommand{is}~~@{text "t :: \<sigma>"}
2235
+ − 499
\end{isabelle}
+ − 500
2237
+ − 501
\noindent
+ − 502
where @{text t} is the definiens (its type @{text \<sigma>} can always be inferred)
+ − 503
and @{text "c"} is the name of definiendum, whose type @{text "\<tau>"} needs to be
+ − 504
given explicitly (the point is that @{text "\<tau>"} and @{text "\<sigma>"} can only differ
2269
+ − 505
in places where a quotient and raw type is involved). Two concrete examples are
2188
+ − 506
2237
+ − 507
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ − 508
\begin{tabular}{@ {}l}
+ − 509
\isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0::nat, 0::nat)"}\\
+ − 510
\isacommand{quotient\_definition}~~@{text "\<Union> :: (\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}~~%
+ − 511
\isacommand{is}~~@{text "flat"}
+ − 512
\end{tabular}
+ − 513
\end{isabelle}
+ − 514
+ − 515
\noindent
+ − 516
The first one declares zero for integers and the second the operator for
2274
+ − 517
building unions of finite sets (@{text "flat"} having the type
+ − 518
@{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"}).
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 519
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 520
The problem for us is that from such declarations we need to derive proper
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 521
definitions using @{text "Abs"} and @{text "Rep"}. The data we rely on is the given quotient type
2247
+ − 522
@{text "\<tau>"} and the raw type @{text "\<sigma>"}. They allow us to define \emph{aggregate
+ − 523
abstraction} and \emph{representation functions} using the functions @{text "ABS (\<sigma>,
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 524
\<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses we shall give below. The idea behind
2274
+ − 525
these two functions is to simultaneously descend into the raw types @{text \<sigma>} and
2247
+ − 526
quotient types @{text \<tau>}, and generate the appropriate
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 527
@{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore
2269
+ − 528
we generate just the identity whenever the types are equal. On the ``way'' down,
+ − 529
however we might have to use map-functions to let @{text Abs} and @{text Rep} act
2274
+ − 530
over the appropriate types. In what follows we use the short-hand notation
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 531
@{text "ABS (\<sigma>s, \<tau>s)"} to mean @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1)\<dots>ABS (\<sigma>\<^isub>n, \<tau>\<^isub>n)"}; similarly
2274
+ − 532
for @{text REP}.
+ − 533
%
2227
+ − 534
\begin{center}
2252
+ − 535
\hfill
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 536
\begin{tabular}{rcl}
2227
+ − 537
\multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 538
@{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 539
@{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\
2227
+ − 540
\multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\
2233
+ − 541
@{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
+ − 542
@{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
2227
+ − 543
\multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\
2232
+ − 544
@{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\
+ − 545
@{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\
2227
+ − 546
\multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 547
@{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s)))"}\\
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 548
@{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s))) \<circ> Rep_\<kappa>\<^isub>q"}
2247
+ − 549
\end{tabular}\hfill\numbered{ABSREP}
2227
+ − 550
\end{center}
2234
+ − 551
%
2232
+ − 552
\noindent
2274
+ − 553
In the last two clauses we have that the type @{text "\<alpha>s
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 554
\<kappa>\<^isub>q"} is the quotient of the raw type @{text "\<rho>s \<kappa>"} (for example
2237
+ − 555
@{text "int"} and @{text "nat \<times> nat"}, or @{text "\<alpha> fset"} and @{text "\<alpha>
+ − 556
list"}). The quotient construction ensures that the type variables in @{text
2247
+ − 557
"\<rho>s"} must be among the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 558
matchers for the @{text "\<alpha>s"} when matching @{text "\<rho>s \<kappa>"} against
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 559
@{text "\<sigma>s \<kappa>"}. The
2237
+ − 560
function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw
+ − 561
type as follows:
+ − 562
%
2227
+ − 563
\begin{center}
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 564
\begin{tabular}{rcl}
2237
+ − 565
@{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a\<^sup>\<alpha>"}\\
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 566
@{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id :: \<kappa> \<Rightarrow> \<kappa>"}\\
2232
+ − 567
@{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\
2233
+ − 568
@{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>as. MAP'(\<sigma>)"}
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 569
\end{tabular}
2227
+ − 570
\end{center}
2237
+ − 571
%
2232
+ − 572
\noindent
2366
+ − 573
In this definition we rely on the fact that in the first clause we can interpret type-variables @{text \<alpha>} as
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 574
term variables @{text a}. In the last clause we build an abstraction over all
2274
+ − 575
term-variables of the map-function generated by the auxiliary function
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 576
@{text "MAP'"}.
2274
+ − 577
The need for aggregate map-functions can be seen in cases where we build quotients,
2247
+ − 578
say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}.
+ − 579
In this case @{text MAP} generates the
+ − 580
aggregate map-function:
2232
+ − 581
2233
+ − 582
@{text [display, indent=10] "\<lambda>a b. map_prod (map a) b"}
+ − 583
+ − 584
\noindent
2274
+ − 585
which is essential in order to define the corresponding aggregate
+ − 586
abstraction and representation functions.
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 587
2247
+ − 588
To see how these definitions pan out in practise, let us return to our
+ − 589
example about @{term "concat"} and @{term "fconcat"}, where we have the raw type
+ − 590
@{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and the quotient type @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>
2274
+ − 591
fset"}. Feeding these types into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)
2247
+ − 592
the abstraction function
2233
+ − 593
+ − 594
@{text [display, indent=10] "(map (map id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map id"}
+ − 595
+ − 596
\noindent
2247
+ − 597
In our implementation we further
+ − 598
simplify this function by rewriting with the usual laws about @{text
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 599
"map"}s and @{text "id"}, namely @{term "map id = id"} and @{text "f \<circ> id =
2274
+ − 600
id \<circ> f = f"}. This gives us the simpler abstraction function
2237
+ − 601
2233
+ − 602
@{text [display, indent=10] "(map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
+ − 603
+ − 604
\noindent
+ − 605
which we can use for defining @{term "fconcat"} as follows
+ − 606
+ − 607
@{text [display, indent=10] "\<Union> \<equiv> ((map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}
2232
+ − 608
2237
+ − 609
\noindent
2247
+ − 610
Note that by using the operator @{text "\<singlearr>"} and special clauses
+ − 611
for function types in \eqref{ABSREP}, we do not have to
2252
+ − 612
distinguish between arguments and results, but can deal with them uniformly.
+ − 613
Consequently, all definitions in the quotient package
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 614
are of the general form
2188
+ − 615
2237
+ − 616
@{text [display, indent=10] "c \<equiv> ABS (\<sigma>, \<tau>) t"}
2227
+ − 617
2237
+ − 618
\noindent
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 619
where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the
2247
+ − 620
type of the defined quotient constant @{text "c"}. This data can be easily
+ − 621
generated from the declaration given by the user.
2252
+ − 622
To increase the confidence in this way of making definitions, we can prove
2247
+ − 623
that the terms involved are all typable.
2227
+ − 624
+ − 625
\begin{lemma}
+ − 626
If @{text "ABS (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"}
+ − 627
and @{text "REP (\<sigma>, \<tau>)"} some representation function @{text "Rep"},
+ − 628
then @{text "Abs"} is of type @{text "\<sigma> \<Rightarrow> \<tau>"} and @{text "Rep"} of type
+ − 629
@{text "\<tau> \<Rightarrow> \<sigma>"}.
+ − 630
\end{lemma}
2233
+ − 631
2237
+ − 632
\begin{proof}
2274
+ − 633
By mutual induction and analysing the definitions of @{text "ABS"} and @{text "REP"}.
+ − 634
The cases of equal types and function types are
2247
+ − 635
straightforward (the latter follows from @{text "\<singlearr>"} having the
+ − 636
type @{text "(\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> (\<gamma> \<Rightarrow> \<delta>) \<Rightarrow> (\<beta> \<Rightarrow> \<gamma>) \<Rightarrow> (\<alpha> \<Rightarrow> \<delta>)"}). In case of equal type
+ − 637
constructors we can observe that a map-function after applying the functions
+ − 638
@{text "ABS (\<sigma>s, \<tau>s)"} produces a term of type @{text "\<sigma>s \<kappa> \<Rightarrow> \<tau>s \<kappa>"}. The
+ − 639
interesting case is the one with unequal type constructors. Since we know
+ − 640
the quotient is between @{text "\<alpha>s \<kappa>\<^isub>q"} and @{text "\<rho>s \<kappa>"}, we have
+ − 641
that @{text "Abs_\<kappa>\<^isub>q"} is of type @{text "\<rho>s \<kappa> \<Rightarrow> \<alpha>s
+ − 642
\<kappa>\<^isub>q"}. This type can be more specialised to @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s
+ − 643
\<kappa>\<^isub>q"} where the type variables @{text "\<alpha>s"} are instantiated with the
+ − 644
@{text "\<tau>s"}. The complete type can be calculated by observing that @{text
+ − 645
"MAP (\<rho>s \<kappa>)"}, after applying the functions @{text "ABS (\<sigma>s', \<tau>s)"} to it,
+ − 646
returns a term of type @{text "\<rho>s[\<sigma>s'] \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}. This type is
+ − 647
equivalent to @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}, which we just have to compose with
+ − 648
@{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"} according to the type of @{text "\<circ>"}.\qed
2237
+ − 649
\end{proof}
2188
+ − 650
*}
+ − 651
2252
+ − 652
section {* Respectfulness and Preservation \label{sec:resp} *}
2188
+ − 653
+ − 654
text {*
2247
+ − 655
The main point of the quotient package is to automatically ``lift'' theorems
+ − 656
involving constants over the raw type to theorems involving constants over
2274
+ − 657
the quotient type. Before we can describe this lifting process, we need to impose
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 658
two restrictions in form of proof obligations that arise during the
2274
+ − 659
lifting. The reason is that even if definitions for all raw constants
+ − 660
can be given, \emph{not} all theorems can be lifted to the quotient type. Most
2287
+ − 661
notable is the bound variable function, that is the constant @{text bn}, defined
2274
+ − 662
for raw lambda-terms as follows
2188
+ − 663
2247
+ − 664
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
2252
+ − 665
@{text "bn (x) \<equiv> \<emptyset>"}\hspace{4mm}
+ − 666
@{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{4mm}
2247
+ − 667
@{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}
+ − 668
\end{isabelle}
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 669
2247
+ − 670
\noindent
2274
+ − 671
We can generate a definition for this constant using @{text ABS} and @{text REP}.
+ − 672
But this constant does \emph{not} respect @{text "\<alpha>"}-equivalence and
2247
+ − 673
consequently no theorem involving this constant can be lifted to @{text
+ − 674
"\<alpha>"}-equated lambda terms. Homeier formulates the restrictions in terms of
2277
+ − 675
the properties of \emph{respectfulness} and \emph{preservation}. We have
2258
+ − 676
to slightly extend Homeier's definitions in order to deal with quotient
2247
+ − 677
compositions.
+ − 678
+ − 679
To formally define what respectfulness is, we have to first define
2287
+ − 680
the notion of \emph{aggregate equivalence relations} using the function @{text REL}:
2274
+ − 681
+ − 682
\begin{center}
+ − 683
\hfill
+ − 684
\begin{tabular}{rcl}
+ − 685
\multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
+ − 686
@{text "REL (\<sigma>, \<sigma>)"} & $\dn$ & @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
+ − 687
\multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\
+ − 688
@{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
+ − 689
\multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\smallskip\\
+ − 690
@{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "rel_\<kappa>\<^isub>q (REL (\<sigma>s', \<tau>s))"}\\
+ − 691
\end{tabular}\hfill\numbered{REL}
+ − 692
\end{center}
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 693
2274
+ − 694
\noindent
+ − 695
The @{text "\<sigma>s'"} in the last clause are calculated as in \eqref{ABSREP}:
+ − 696
we know that type @{text "\<alpha>s \<kappa>\<^isub>q"} is the quotient of the raw type
+ − 697
@{text "\<rho>s \<kappa>"}. The @{text "\<sigma>s'"} are determined by matching
+ − 698
@{text "\<rho>s \<kappa>"} and @{text "\<sigma>s \<kappa>"}.
+ − 699
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 700
Let us return to the lifting procedure of theorems. Assume we have a theorem
2274
+ − 701
that contains the raw constant @{text "c\<^isub>r :: \<sigma>"} and which we want to
+ − 702
lift to a theorem where @{text "c\<^isub>r"} is replaced by the corresponding
+ − 703
constant @{text "c\<^isub>q :: \<tau>"} defined over a quotient type. In this situation
2287
+ − 704
we generate the following proof obligation
2274
+ − 705
+ − 706
@{text [display, indent=10] "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
2258
+ − 707
2274
+ − 708
\noindent
2277
+ − 709
Homeier calls these proof obligations \emph{respectfulness
2278
+ − 710
theorems}. However, unlike his quotient package, we might have several
+ − 711
respectfulness theorems for one constant---he has at most one.
+ − 712
The reason is that because of our quotient compositions, the types
+ − 713
@{text \<sigma>} and @{text \<tau>} are not completely determined by the type of @{text "c\<^bsub>r\<^esub>"}.
+ − 714
And for every instantiation of the types, we might end up with a
+ − 715
corresponding respectfulness theorem.
+ − 716
+ − 717
Before lifting a theorem, we require the user to discharge
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 718
respectfulness proof obligations. In case of @{text bn}
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 719
this obligation is as follows
2274
+ − 720
+ − 721
@{text [display, indent=10] "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
+ − 722
+ − 723
\noindent
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 724
and the point is that the user cannot discharge it: because it is not true. To see this,
2274
+ − 725
we can just unfold the definition of @{text "\<doublearr>"} \eqref{relfun}
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 726
using extensionally to obtain the false statement
2274
+ − 727
+ − 728
@{text [display, indent=10] "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 implies bn(t\<^isub>1) = bn(t\<^isub>2)"}
+ − 729
+ − 730
\noindent
+ − 731
In contrast, if we lift a theorem about @{text "append"} to a theorem describing
+ − 732
the union of finite sets, then we need to discharge the proof obligation
+ − 733
2275
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 734
@{text [display, indent=10] "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 735
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 736
\noindent
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 737
To do so, we have to establish
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 738
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 739
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
2287
+ − 740
if @{text "xs \<approx>\<^bsub>list\<^esub> ys"} and @{text "us \<approx>\<^bsub>list\<^esub> vs"}
+ − 741
then @{text "xs @ us \<approx>\<^bsub>list\<^esub> ys @ vs"}
2275
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 742
\end{isabelle}
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 743
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 744
\noindent
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 745
which is straightforward given the definition shown in \eqref{listequiv}.
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 746
2333
+ − 747
The second restriction we have to impose arises from non-lifted polymorphic
+ − 748
constants, which are instantiated to a type being quotient. For example,
+ − 749
take the @{term "cons"}-constructor to add a pair of natural numbers to a
+ − 750
list, whereby we assume the pair of natural numbers turns into an integer in
+ − 751
the quotient construction. The point is that we still want to use @{text
+ − 752
cons} for adding integers to lists---just with a different type. To be able
+ − 753
to lift such theorems, we need a \emph{preservation property} for @{text
+ − 754
cons}. Assuming we have a polymorphic raw constant @{text "c\<^isub>r :: \<sigma>"}
+ − 755
and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"}, then a
+ − 756
preservation property is as follows
+ − 757
2275
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 758
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 759
@{text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"}
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 760
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 761
\noindent
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 762
where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}.
2278
+ − 763
In case of @{text cons} (which has type @{text "\<alpha> \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"}) we have
2275
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 764
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 765
@{text [display, indent=10] "(Rep ---> map Rep ---> map Abs) cons = cons"}
2274
+ − 766
+ − 767
\noindent
2278
+ − 768
under the assumption @{text "Quotient R Abs Rep"}. Interestingly, if we have
+ − 769
an instance of @{text cons} where the type variable @{text \<alpha>} is instantiated
+ − 770
with @{text "nat \<times> nat"} and we also quotient this type to yield integers,
2287
+ − 771
then we need to show the corresponding preservation property.
2274
+ − 772
2279
+ − 773
%%%@ {thm [display, indent=10] insert_preserve2[no_vars]}
2189
+ − 774
2278
+ − 775
%Given two quotients, one of which quotients a container, and the
+ − 776
%other quotients the type in the container, we can write the
+ − 777
%composition of those quotients. To compose two quotient theorems
+ − 778
%we compose the relations with relation composition as defined above
+ − 779
%and the abstraction and relation functions are the ones of the sub
+ − 780
%quotients composed with the usual function composition.
+ − 781
%The @ {term "Rep"} and @ {term "Abs"} functions that we obtain agree
+ − 782
%with the definition of aggregate Abs/Rep functions and the
+ − 783
%relation is the same as the one given by aggregate relations.
+ − 784
%This becomes especially interesting
+ − 785
%when we compose the quotient with itself, as there is no simple
+ − 786
%intermediate step.
+ − 787
%
+ − 788
%Lets take again the example of @ {term flat}. To be able to lift
+ − 789
%theorems that talk about it we provide the composition quotient
+ − 790
%theorem which allows quotienting inside the container:
+ − 791
%
+ − 792
%If @ {term R} is an equivalence relation and @ {term "Quotient R Abs Rep"}
+ − 793
%then
+ − 794
%
+ − 795
%@ {text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep o rep_fset)"}
2275
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 796
%%%
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 797
%%%\noindent
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 798
%%%this theorem will then instantiate the quotients needed in the
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 799
%%%injection and cleaning proofs allowing the lifting procedure to
69b80ad616c5
finished section 4, but put some things I do not understand on comment
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 800
%%%proceed in an unchanged way.
2192
+ − 801
*}
+ − 802
2256
+ − 803
section {* Lifting of Theorems\label{sec:lift} *}
1978
+ − 804
2194
+ − 805
text {*
2271
+ − 806
2278
+ − 807
The main benefit of a quotient package is to lift automatically theorems over raw
+ − 808
types to theorems over quotient types. We will perform this lifting in
+ − 809
three phases, called \emph{regularization},
2287
+ − 810
\emph{injection} and \emph{cleaning} according to procedures in Homeier's ML-code.
2271
+ − 811
2278
+ − 812
The purpose of regularization is to change the quantifiers and abstractions
+ − 813
in a ``raw'' theorem to quantifiers over variables that respect the relation
2279
+ − 814
(Definition \ref{def:respects} states what respects means). The purpose of injection is to add @{term Rep}
2271
+ − 815
and @{term Abs} of appropriate types in front of constants and variables
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 816
of the raw type so that they can be replaced by the corresponding constants from the
2279
+ − 817
quotient type. The purpose of cleaning is to bring the theorem derived in the
+ − 818
first two phases into the form the user has specified. Abstractly, our
+ − 819
package establishes the following three proof steps:
+ − 820
+ − 821
\begin{center}
+ − 822
\begin{tabular}{r@ {\hspace{4mm}}l}
+ − 823
1.) & @{text "raw_thm \<longrightarrow> reg_thm"}\\
+ − 824
2.) & @{text "reg_thm \<longleftrightarrow> inj_thm"}\\
+ − 825
3.) & @{text "inj_thm \<longleftrightarrow> quot_thm"}\\
+ − 826
\end{tabular}
+ − 827
\end{center}
2193
+ − 828
2279
+ − 829
\noindent
2287
+ − 830
which means the raw theorem implies the quotient theorem.
2279
+ − 831
In contrast to other quotient packages, our package requires
+ − 832
the \emph{term} of the @{text "quot_thm"} to be given by the user.\footnote{Though we
+ − 833
also provide a fully automated mode, where the @{text "quot_thm"} is guessed
2287
+ − 834
from the form of @{text "raw_thm"}.} As a result, it is possible that a user can lift only some
+ − 835
occurrences of a raw type, but not others.
2279
+ − 836
+ − 837
The second and third proof step will always succeed if the appropriate
+ − 838
respectfulness and preservation theorems are given. In contrast, the first
+ − 839
proof step can fail: a theorem given by the user does not always
2319
+ − 840
imply a regularized version and a stronger one needs to be proved. An example
2287
+ − 841
for this kind of failure is the simple statement for integers @{text "0 \<noteq> 1"}.
+ − 842
One might hope that it can be proved by lifting @{text "(0, 0) \<noteq> (1, 0)"},
2319
+ − 843
but this raw theorem only shows that particular element in the
+ − 844
equivalence classes are not equal. In order to obtain @{text "0 \<noteq> 1"}, a
+ − 845
more general statement stipulating that the equivalence classes are not
+ − 846
equal is necessary. This kind of failure is beyond the scope where the
+ − 847
quotient package can help: the user has to provide a raw theorem that
+ − 848
can be regularized automatically, or has to provide an explicit proof
+ − 849
for the first proof step.
2193
+ − 850
2271
+ − 851
In the following we will first define the statement of the
2280
229660b9f2fc
Fix regularization. Two "FIXME" left in introduction. Minor spellings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 852
regularized theorem based on @{text "raw_thm"} and
2279
+ − 853
@{text "quot_thm"}. Then we define the statement of the injected theorem, based
2287
+ − 854
on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps,
2279
+ − 855
which can all be performed independently from each other.
2197
+ − 856
2287
+ − 857
We first define the function @{text REG}. The intuition
2207
+ − 858
behind this function is that it replaces quantifiers and
+ − 859
abstractions involving raw types by bounded ones, and equalities
+ − 860
involving raw types are replaced by appropriate aggregate
2251
+ − 861
equivalence relations. It is defined as follows:
1994
+ − 862
2244
+ − 863
\begin{center}
2273
+ − 864
\begin{longtable}{rcl}
+ − 865
\multicolumn{3}{@ {}l}{abstractions:}\smallskip\\
+ − 866
@{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} & $\dn$ &
+ − 867
$\begin{cases}
+ − 868
@{text "\<lambda>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+ − 869
@{text "\<lambda>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
+ − 870
\end{cases}$\smallskip\\
2279
+ − 871
\\
2273
+ − 872
\multicolumn{3}{@ {}l}{universal quantifiers:}\\
+ − 873
@{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} & $\dn$ &
+ − 874
$\begin{cases}
+ − 875
@{text "\<forall>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+ − 876
@{text "\<forall>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
+ − 877
\end{cases}$\smallskip\\
+ − 878
\multicolumn{3}{@ {}l}{equality:}\smallskip\\
2280
229660b9f2fc
Fix regularization. Two "FIXME" left in introduction. Minor spellings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 879
%% REL of two equal types is the equality so we do not need a separate case
229660b9f2fc
Fix regularization. Two "FIXME" left in introduction. Minor spellings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 880
@{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>)"}\\\smallskip\\
2273
+ − 881
\multicolumn{3}{@ {}l}{applications, variables and constants:}\\
2244
+ − 882
@{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} & $\dn$ & @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
2273
+ − 883
@{text "REG (x\<^isub>1, x\<^isub>2)"} & $\dn$ & @{text "x\<^isub>1"}\\
+ − 884
@{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\[-5mm]
+ − 885
\end{longtable}
2244
+ − 886
\end{center}
2273
+ − 887
%
+ − 888
\noindent
2230
+ − 889
In the above definition we omitted the cases for existential quantifiers
2207
+ − 890
and unique existential quantifiers, as they are very similar to the cases
2333
+ − 891
for the universal quantifier. For the third and fourth clause, note that
2287
+ − 892
@{text "\<forall>x. P"} is defined as @{text "\<forall> (\<lambda>x. P)"}.
2279
+ − 893
+ − 894
Next we define the function @{text INJ} which takes as argument
+ − 895
@{text "reg_thm"} and @{text "quot_thm"} (both as
+ − 896
terms) and returns @{text "inj_thm"}:
2198
+ − 897
2245
+ − 898
\begin{center}
+ − 899
\begin{tabular}{rcl}
2273
+ − 900
\multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions:}\\
+ − 901
@{text "INJ (\<lambda>x. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$ &
+ − 902
$\begin{cases}
+ − 903
@{text "\<lambda>x. INJ (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+ − 904
@{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x. INJ (t, s)))"}
+ − 905
\end{cases}$\\
+ − 906
@{text "INJ (\<lambda>x \<in> R. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$
+ − 907
& @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x \<in> R. INJ (t, s)))"}\smallskip\\
+ − 908
\multicolumn{3}{@ {\hspace{-4mm}}l}{universal quantifiers:}\\
+ − 909
@{text "INJ (\<forall> t, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s)"}\\
+ − 910
@{text "INJ (\<forall> t \<in> R, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s) \<in> R"}\smallskip\\
+ − 911
\multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables and constants:}\smallskip\\
2245
+ − 912
@{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) "} & $\dn$ & @{text " INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}\\
2273
+ − 913
@{text "INJ (x\<^isub>1\<^sup>\<sigma>, x\<^isub>2\<^sup>\<tau>) "} & $\dn$ &
+ − 914
$\begin{cases}
+ − 915
@{text "x\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+ − 916
@{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) x\<^isub>1)"}\\
+ − 917
\end{cases}$\\
+ − 918
@{text "INJ (c\<^isub>1\<^sup>\<sigma>, c\<^isub>2\<^sup>\<tau>) "} & $\dn$ &
+ − 919
$\begin{cases}
+ − 920
@{text "c\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+ − 921
@{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) c\<^isub>1)"}\\
+ − 922
\end{cases}$\\
2245
+ − 923
\end{tabular}
+ − 924
\end{center}
2198
+ − 925
2279
+ − 926
\noindent
2319
+ − 927
In this definition we again omitted the cases for existential and unique existential
+ − 928
quantifiers.
2208
+ − 929
2279
+ − 930
In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always
+ − 931
start with an implication. Isabelle provides \emph{mono} rules that can split up
2319
+ − 932
the implications into simpler implicational subgoals. This succeeds for every
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 933
monotone connective, except in places where the function @{text REG} replaced,
2287
+ − 934
for instance, a quantifier by a bounded quantifier. In this case we have
2279
+ − 935
rules of the form
2208
+ − 936
2279
+ − 937
@{text [display, indent=10] "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}
+ − 938
+ − 939
\noindent
2280
229660b9f2fc
Fix regularization. Two "FIXME" left in introduction. Minor spellings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 940
They decompose a bounded quantifier on the right-hand side. We can decompose a
229660b9f2fc
Fix regularization. Two "FIXME" left in introduction. Minor spellings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 941
bounded quantifier anywhere if R is an equivalence relation or
229660b9f2fc
Fix regularization. Two "FIXME" left in introduction. Minor spellings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 942
if it is a relation over function types with the range being an equivalence
229660b9f2fc
Fix regularization. Two "FIXME" left in introduction. Minor spellings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 943
relation. If @{text R} is an equivalence relation we can prove that
2261
+ − 944
2279
+ − 945
@{text [display, indent=10] "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}
2199
+ − 946
2279
+ − 947
\noindent
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 948
If @{term R\<^isub>2} is an equivalence relation, we can prove
2231
+ − 949
2273
+ − 950
@{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
2209
+ − 951
2279
+ − 952
\noindent
2242
+ − 953
The last theorem is new in comparison with Homeier's package. There the
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 954
injection procedure would be used to prove such goals and
2279
+ − 955
the assumption about the equivalence relation would be used. We use the above theorem directly,
+ − 956
because this allows us to completely separate the first and the second
2287
+ − 957
proof step into two independent ``units''.
2206
+ − 958
2280
229660b9f2fc
Fix regularization. Two "FIXME" left in introduction. Minor spellings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 959
The second proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"}, starts with an equality.
2279
+ − 960
The proof again follows the structure of the
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 961
two underlying terms and is defined for a goal being a relation between these two terms.
2199
+ − 962
2211
+ − 963
\begin{itemize}
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 964
\item For two constants an appropriate respectfulness theorem is applied.
2279
+ − 965
\item For two variables, we use the assumptions proved in the regularization step.
+ − 966
\item For two abstractions, we @{text "\<eta>"}-expand and @{text "\<beta>"}-reduce them.
+ − 967
\item For two applications, we check that the right-hand side is an application of
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 968
@{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"} holds. If yes then we
2279
+ − 969
can apply the theorem:
2271
+ − 970
+ − 971
@{term [display, indent=10] "R x y \<longrightarrow> R x (Rep (Abs y))"}
+ − 972
2279
+ − 973
Otherwise we introduce an appropriate relation between the subterms
2271
+ − 974
and continue with two subgoals using the lemma:
+ − 975
2273
+ − 976
@{text [display, indent=10] "(R\<^isub>1 \<doublearr> R\<^isub>2) f g \<longrightarrow> R\<^isub>1 x y \<longrightarrow> R\<^isub>2 (f x) (g y)"}
2211
+ − 977
\end{itemize}
2199
+ − 978
2279
+ − 979
We defined the theorem @{text "inj_thm"} in such a way that
+ − 980
establishing the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be
+ − 981
achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient
2287
+ − 982
definitions. Then for all lifted constants, their definitions
2271
+ − 983
are used to fold the @{term Rep} with the raw constant. Next for
2279
+ − 984
all abstractions and quantifiers the lambda and
2271
+ − 985
quantifier preservation theorems are used to replace the
2279
+ − 986
variables that include raw types with respects by quantifiers
2271
+ − 987
over variables that include quotient types. We show here only
2279
+ − 988
the lambda preservation theorem. Given
+ − 989
@{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}, we have:
2211
+ − 990
2279
+ − 991
@{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
2199
+ − 992
2243
+ − 993
\noindent
2279
+ − 994
Next, relations over lifted types are folded to equalities.
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 995
For this the following theorem has been shown by Homeier~\cite{Homeier05}:
2211
+ − 996
2271
+ − 997
@{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]}
2199
+ − 998
2271
+ − 999
\noindent
2279
+ − 1000
Finally, we rewrite with the preservation theorems. This will result
+ − 1001
in two equal terms that can be solved by reflexivity.
2246
+ − 1002
*}
1994
+ − 1003
2274
+ − 1004
section {* Examples \label{sec:examples} *}
1994
+ − 1005
2210
+ − 1006
(* Mention why equivalence *)
2206
+ − 1007
2210
+ − 1008
text {*
+ − 1009
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1010
In this section we will show a sequence of declarations for defining the
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1011
type of integers by quotienting pairs of natural numbers, and
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1012
lifting one theorem.
2210
+ − 1013
2240
+ − 1014
A user of our quotient package first needs to define a relation on
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1015
the raw type with which the quotienting will be performed. We give
2279
+ − 1016
the same integer relation as the one presented in \eqref{natpairequiv}:
2240
+ − 1017
+ − 1018
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
2279
+ − 1019
\begin{tabular}{@ {}l}
+ − 1020
\isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"}\\
+ − 1021
\isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"}
+ − 1022
\end{tabular}
2239
+ − 1023
\end{isabelle}
2210
+ − 1024
2239
+ − 1025
\noindent
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1026
Next the quotient type must be defined. This generates a proof obligation that the
2279
+ − 1027
relation is an equivalence relation, which is solved automatically using the
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1028
definition of equivalence and extensionality:
2210
+ − 1029
2240
+ − 1030
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
2279
+ − 1031
\begin{tabular}{@ {}l}
+ − 1032
\isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"}\\
+ − 1033
\hspace{5mm}@{text "by (auto simp add: equivp_def expand_fun_eq)"}
+ − 1034
\end{tabular}
2239
+ − 1035
\end{isabelle}
2210
+ − 1036
2239
+ − 1037
\noindent
2210
+ − 1038
The user can then specify the constants on the quotient type:
+ − 1039
2240
+ − 1040
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+ − 1041
\begin{tabular}{@ {}l}
2279
+ − 1042
\isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\[3mm]
2287
+ − 1043
\isacommand{fun}~~@{text "add_pair"}~~\isacommand{where}~~%
+ − 1044
@{text "add_pair (m, n) (p, q) \<equiv> (m + p :: nat, n + q :: nat)"}\\
2273
+ − 1045
\isacommand{quotient\_definition}~~@{text "+ :: int \<Rightarrow> int \<Rightarrow> int"}~~%
2287
+ − 1046
\isacommand{is}~~@{text "add_pair"}\\
2240
+ − 1047
\end{tabular}
+ − 1048
\end{isabelle}
2210
+ − 1049
2240
+ − 1050
\noindent
2279
+ − 1051
The following theorem about addition on the raw level can be proved.
2210
+ − 1052
2240
+ − 1053
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
2287
+ − 1054
\isacommand{lemma}~~@{text "add_pair_zero: int_rel (add_pair (0, 0) x) x"}
2240
+ − 1055
\end{isabelle}
2210
+ − 1056
2240
+ − 1057
\noindent
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1058
If the user lifts this theorem, all proof obligations are
2279
+ − 1059
automatically discharged, except the respectfulness
2287
+ − 1060
proof for @{text "add_pair"}:
2210
+ − 1061
2240
+ − 1062
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
2279
+ − 1063
\begin{tabular}{@ {}l}
2287
+ − 1064
\isacommand{lemma}~~@{text "[quot_respect]:"}\\
+ − 1065
@{text "(int_rel \<doublearr> int_rel \<doublearr> int_rel) add_pair add_pair"}
2279
+ − 1066
\end{tabular}
2240
+ − 1067
\end{isabelle}
+ − 1068
+ − 1069
\noindent
2333
+ − 1070
This property needs to be proved by the user. It
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1071
can be discharged automatically by Isabelle when hinting to unfold the definition
2273
+ − 1072
of @{text "\<doublearr>"}.
2332
9a560e489c64
polished paper again (and took out some claims about Homeier's package)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1073
After this, the user can prove the lifted lemma as follows:
2210
+ − 1074
2240
+ − 1075
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
2287
+ − 1076
\isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting add_pair_zero"}
2240
+ − 1077
\end{isabelle}
2210
+ − 1078
2240
+ − 1079
\noindent
2333
+ − 1080
or by using the completely automated mode stating just:
2210
+ − 1081
2240
+ − 1082
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
2287
+ − 1083
\isacommand{thm}~~@{text "add_pair_zero[quot_lifted]"}
2240
+ − 1084
\end{isabelle}
2210
+ − 1085
2240
+ − 1086
\noindent
2279
+ − 1087
Both methods give the same result, namely
+ − 1088
+ − 1089
@{text [display, indent=10] "0 + x = x"}
+ − 1090
+ − 1091
\noindent
2333
+ − 1092
where @{text x} is of type integer.
2279
+ − 1093
Although seemingly simple, arriving at this result without the help of a quotient
2333
+ − 1094
package requires a substantial reasoning effort (see \cite{Paulson06}).
2210
+ − 1095
*}
2206
+ − 1096
2256
+ − 1097
section {* Conclusion and Related Work\label{sec:conc}*}
1978
+ − 1098
+ − 1099
text {*
2243
+ − 1100
2333
+ − 1101
The code of the quotient package and the examples described here are already
+ − 1102
included in the standard distribution of Isabelle.\footnote{Available from
+ − 1103
\href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} The package is
+ − 1104
heavily used in the new version of Nominal Isabelle, which provides a
+ − 1105
convenient reasoning infrastructure for programming language calculi
+ − 1106
involving general binders. To achieve this, it builds types representing
+ − 1107
@{text \<alpha>}-equivalent terms. Earlier versions of Nominal Isabelle have been
+ − 1108
used successfully in formalisations of an equivalence checking algorithm for
+ − 1109
LF \cite{UrbanCheneyBerghofer08}, Typed
+ − 1110
Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
+ − 1111
\cite{BengtsonParow09} and a strong normalisation result for cut-elimination
+ − 1112
in classical logic \cite{UrbanZhu08}.
+ − 1113
2237
+ − 1114
2333
+ − 1115
There is a wide range of existing literature for dealing with quotients
+ − 1116
in theorem provers. Slotosch~\cite{Slotosch97} implemented a mechanism that
+ − 1117
automatically defines quotient types for Isabelle/HOL. But he did not
+ − 1118
include theorem lifting. Harrison's quotient package~\cite{harrison-thesis}
+ − 1119
is the first one that is able to automatically lift theorems, however only
+ − 1120
first-order theorems (that is theorems where abstractions, quantifiers and
+ − 1121
variables do not involve functions that include the quotient type). There is
+ − 1122
also some work on quotient types in non-HOL based systems and logical
+ − 1123
frameworks, including theory interpretations in
+ − 1124
PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, and
+ − 1125
setoids in Coq \cite{ChicliPS02}. Paulson showed a construction of
+ − 1126
quotients that does not require the Hilbert Choice operator, but also only
+ − 1127
first-order theorems can be lifted~\cite{Paulson06}. The most related work
+ − 1128
to our package is the package for HOL4 by Homeier~\cite{Homeier05}. He
+ − 1129
introduced most of the abstract notions about quotients and also deals with
+ − 1130
lifting of higher-order theorems. However, he cannot deal with quotient
+ − 1131
compositions (needed for lifting theorems about @{text flat}). Also, a
+ − 1132
number of his definitions, like @{text ABS}, @{text REP} and @{text INJ} etc
+ − 1133
only exist in \cite{Homeier05} as ML-code, not included in the paper.
2334
+ − 1134
Like Homeier's, our quotient package can deal with partial equivalence
+ − 1135
relations, but for lack of space we do not describe the mechanisms
+ − 1136
needed for this kind of quotient constructions.
2224
+ − 1137
2333
+ − 1138
+ − 1139
One feature of our quotient package is that when lifting theorems, the user
+ − 1140
can precisely specify what the lifted theorem should look like. This feature
+ − 1141
is necessary, for example, when lifting an induction principle for two
+ − 1142
lists. Assuming this principle has as the conclusion a predicate of the
+ − 1143
form @{text "P xs ys"}, then we can precisely specify whether we want to
+ − 1144
quotient @{text "xs"} or @{text "ys"}, or both. We found this feature very
+ − 1145
useful in the new version of Nominal Isabelle, where such a choice is
+ − 1146
required to generate a reasoning infrastructure for alpha-equated terms.
2287
+ − 1147
%%
+ − 1148
%% give an example for this
+ − 1149
%%
2278
+ − 1150
\medskip
2224
+ − 1151
2263
+ − 1152
\noindent
2287
+ − 1153
{\bf Acknowledgements:} We would like to thank Peter Homeier for the many
2277
+ − 1154
discussions about his HOL4 quotient package and explaining to us
2283
+ − 1155
some of its finer points in the implementation. Without his patient
+ − 1156
help, this work would have been impossible.
2263
+ − 1157
2224
+ − 1158
*}
+ − 1159
+ − 1160
2227
+ − 1161
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 1162
(*<*)
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 1163
end
1978
+ − 1164
(*>*)