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