(* How to change the notation for \<lbrakk> \<rbrakk> meta-level implications? *)+ −
+ −
(*<*)+ −
theory Paper+ −
imports "Quotient"+ −
"LaTeXsugar"+ −
"../Nominal/FSet"+ −
begin+ −
+ −
notation (latex output)+ −
rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and+ −
pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and+ −
"op -->" (infix "\<longrightarrow>" 100) and+ −
"==>" (infix "\<Longrightarrow>" 100) and+ −
fun_map ("_ \<^raw:\mbox{\singlearr}> _" 51) and+ −
fun_rel ("_ \<^raw:\mbox{\doublearr}> _" 51) and+ −
list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)+ −
fempty ("\<emptyset>") and+ −
funion ("_ \<union> _") and+ −
finsert ("{_} \<union> _") and + −
Cons ("_::_") and+ −
concat ("flat") and+ −
fconcat ("\<Union>")+ −
+ −
+ −
+ −
ML {*+ −
fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;+ −
fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>+ −
let+ −
val concl =+ −
Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)+ −
in+ −
case concl of (_ $ l $ r) => proj (l, r)+ −
| _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)+ −
end);+ −
*}+ −
setup {*+ −
Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #>+ −
Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #>+ −
Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))+ −
*}+ −
(*>*)+ −
+ −
+ −
section {* Introduction *}+ −
+ −
text {* + −
\begin{flushright}+ −
{\em ``Not using a [quotient] package has its advantages: we do not have to\\ + −
collect all the theorems we shall ever want into one giant list;''}\\+ −
Larry Paulson \cite{Paulson06}+ −
\end{flushright}+ −
+ −
\noindent+ −
Isabelle is a popular generic theorem prover in which many logics can be+ −
implemented. The most widely used one, however, is Higher-Order Logic+ −
(HOL). This logic consists of a small number of axioms and inference rules+ −
over a simply-typed term-language. Safe reasoning in HOL is ensured by two+ −
very restricted mechanisms for extending the logic: one is the definition of+ −
new constants in terms of existing ones; the other is the introduction of+ −
new types by identifying non-empty subsets in existing types. It is well+ −
understood how to use both mechanisms for dealing with quotient+ −
constructions in HOL (see \cite{Homeier05,Paulson06}). For example the+ −
integers in Isabelle/HOL are constructed by a quotient construction over the+ −
type @{typ "nat \<times> nat"} and the equivalence relation+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
@{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}+ −
\end{isabelle}+ −
+ −
\noindent+ −
This constructions yields the new type @{typ int} and definitions for @{text+ −
"0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of+ −
natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations+ −
such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in+ −
terms of operations on pairs of natural numbers (namely @{text+ −
"add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2,+ −
m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}).+ −
Similarly one can construct the type of finite sets, written @{term "\<alpha> fset"}, + −
by quotienting the type @{text "\<alpha> list"} according to the equivalence relation+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
@{text "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}\hfill\numbered{listequiv}+ −
\end{isabelle}+ −
+ −
\noindent+ −
which states that two lists are equivalent if every element in one list is+ −
also member in the other. The empty finite set, written @{term "{||}"}, can+ −
then be defined as the empty list and the union of two finite sets, written+ −
@{text "\<union>"}, as list append.+ −
+ −
Quotients are important in a variety of areas, but they are really ubiquitous in+ −
the area of reasoning about programming language calculi. A simple example+ −
is the lambda-calculus, whose raw terms are defined as+ −
+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
@{text "t ::= x | t t | \<lambda>x.t"}\hfill\numbered{lambda}+ −
\end{isabelle}+ −
+ −
\noindent+ −
The problem with this definition arises, for instance, when one attempts to+ −
prove formally the substitution lemma \cite{Barendregt81} by induction+ −
over the structure of terms. This can be fiendishly complicated (see+ −
\cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof+ −
about raw lambda-terms). In contrast, if we reason about+ −
$\alpha$-equated lambda-terms, that means terms quotient according to+ −
$\alpha$-equivalence, then the reasoning infrastructure provided, + −
for example, by Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal + −
proof of the substitution lemma almost trivial. + −
+ −
The difficulty is that in order to be able to reason about integers, finite+ −
sets or $\alpha$-equated lambda-terms one needs to establish a reasoning+ −
infrastructure by transferring, or \emph{lifting}, definitions and theorems+ −
from the raw type @{typ "nat \<times> nat"} to the quotient type @{typ int}+ −
(similarly for finite sets and $\alpha$-equated lambda-terms). This lifting+ −
usually requires a \emph{lot} of tedious reasoning effort \cite{Paulson06}. + −
It is feasible to do this work manually, if one has only a few quotient+ −
constructions at hand. But if they have to be done over and over again, as in + −
Nominal Isabelle, then manual reasoning is not an option.+ −
+ −
The purpose of a \emph{quotient package} is to ease the lifting of theorems+ −
and automate the reasoning as much as possible. In the+ −
context of HOL, there have been a few quotient packages already+ −
\cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier+ −
\cite{Homeier05} implemented in HOL4. The fundamental construction these+ −
quotient packages perform can be illustrated by the following picture:+ −
+ −
\begin{center}+ −
\mbox{}\hspace{20mm}\begin{tikzpicture}+ −
%%\draw[step=2mm] (-4,-1) grid (4,1);+ −
+ −
\draw[very thick] (0.7,0.3) circle (4.85mm);+ −
\draw[rounded corners=1mm, very thick] ( 0.0,-0.9) rectangle ( 1.8, 0.9);+ −
\draw[rounded corners=1mm, very thick] (-1.95,0.8) rectangle (-2.9,-0.195);+ −
+ −
\draw (-2.0, 0.8) -- (0.7,0.8);+ −
\draw (-2.0,-0.195) -- (0.7,-0.195);+ −
+ −
\draw ( 0.7, 0.23) node {\begin{tabular}{@ {}c@ {}}equiv-\\[-1mm]clas.\end{tabular}};+ −
\draw (-2.45, 0.35) node {\begin{tabular}{@ {}c@ {}}new\\[-1mm]type\end{tabular}};+ −
\draw (1.8, 0.35) node[right=-0.1mm]+ −
{\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw elements)\end{tabular}};+ −
\draw (0.9, -0.55) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};+ −
+ −
\draw[->, very thick] (-1.8, 0.36) -- (-0.1,0.36);+ −
\draw[<-, very thick] (-1.8, 0.16) -- (-0.1,0.16);+ −
\draw (-0.95, 0.26) node[above=0.4mm] {@{text Rep}};+ −
\draw (-0.95, 0.26) node[below=0.4mm] {@{text Abs}};+ −
+ −
\end{tikzpicture}+ −
\end{center}+ −
+ −
\noindent+ −
The starting point is an existing type, to which we refer as the+ −
\emph{raw type} and over which an equivalence relation given by the user is+ −
defined. With this input the package introduces a new type, to which we+ −
refer as the \emph{quotient type}. This type comes with an+ −
\emph{abstraction} and a \emph{representation} function, written @{text Abs}+ −
and @{text Rep}.\footnote{Actually slightly more basic functions are given;+ −
the functions @{text Abs} and @{text Rep} need to be derived from them. We+ −
will show the details later. } They relate elements in the+ −
existing type to elements in the new type and vice versa, and can be uniquely+ −
identified by their quotient type. For example for the integer quotient construction+ −
the types of @{text Abs} and @{text Rep} are+ −
+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
@{text "Abs :: nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep :: int \<Rightarrow> nat \<times> nat"}+ −
\end{isabelle}+ −
+ −
\noindent+ −
We therefore often write @{text Abs_int} and @{text Rep_int} if the+ −
typing information is important. + −
+ −
Every abstraction and representation function stands for an isomorphism+ −
between the non-empty subset and elements in the new type. They are+ −
necessary for making definitions involving the new type. For example @{text+ −
"0"} and @{text "1"} of type @{typ int} can be defined as+ −
+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
@{text "0 \<equiv> Abs_int (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs_int (1, 0)"}+ −
\end{isabelle}+ −
+ −
\noindent+ −
Slightly more complicated is the definition of @{text "add"} having type + −
@{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition is as follows+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
@{text "add n m \<equiv> Abs_int (add_pair (Rep_int n) (Rep_int m))"}+ −
\hfill\numbered{adddef}+ −
\end{isabelle}+ −
+ −
\noindent+ −
where we take the representation of the arguments @{text n} and @{text m},+ −
add them according to the function @{text "add_pair"} and then take the+ −
abstraction of the result. This is all straightforward and the existing+ −
quotient packages can deal with such definitions. But what is surprising+ −
that none of them can deal with slightly more complicated definitions involving+ −
\emph{compositions} of quotients. Such compositions are needed for example+ −
in case of quotienting lists to yield finite sets and the operator that + −
flattens lists of lists, defined as follows+ −
+ −
@{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]}+ −
+ −
\noindent+ −
We expect that the corresponding operator on finite sets, written @{term "fconcat"},+ −
builds finite unions of finite sets:+ −
+ −
@{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}+ −
+ −
\noindent+ −
The quotient package should automatically provide us with a definition for @{text "\<Union>"} in+ −
terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is + −
that the method used in the existing quotient+ −
packages of just taking the representation of the arguments and then taking+ −
the abstraction of the result is \emph{not} enough. The reason is that in case+ −
of @{text "\<Union>"} we obtain the incorrect definition+ −
+ −
@{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}+ −
+ −
\noindent+ −
where the right-hand side is not even typable! This problem can be remedied in the+ −
existing quotient packages by introducing an intermediate step and reasoning+ −
about flattening of lists of finite sets. However, this remedy is rather+ −
cumbersome and inelegant in light of our work, which can deal with such+ −
definitions directly. The solution is that we need to build aggregate+ −
representation and abstraction functions, which in case of @{text "\<Union>"}+ −
generate the following definition+ −
+ −
@{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat ((map Rep_fset \<circ> Rep_fset) S))"}+ −
+ −
\noindent+ −
where @{term map} is the usual mapping function for lists. In this paper we+ −
will present a formal definition of our aggregate abstraction and+ −
representation functions (this definition was omitted in \cite{Homeier05}). + −
They generate definitions, like the one above for @{text "\<Union>"}, + −
according to the type of the raw constant and the type+ −
of the quotient constant. This means we also have to extend the notions+ −
of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}+ −
from Homeier \cite{Homeier05}.+ −
+ −
In addition we are able to address the criticism by Paulson \cite{Paulson06} cited+ −
at the beginning of this section about having to collect theorems that are+ −
lifted from the raw level to the quotient level into one giant list. Our+ −
quotient package is the first one that is modular so that it allows to lift+ −
single theorems separately. This has the advantage for the user of being able to develop a+ −
formal theory interactively as a natural progression. A pleasing side-result of+ −
the modularity is that we are able to clearly specify what is involved+ −
in the lifting process (this was only hinted at in \cite{Homeier05} and+ −
implemented as a ``rough recipe'' in ML-code).+ −
+ −
+ −
The paper is organised as follows: Section \ref{sec:prelims} presents briefly+ −
some necessary preliminaries; Section \ref{sec:type} describes the definitions + −
of quotient types and shows how definitions of constants can be made over + −
quotient types. Section \ref{sec:resp} introduces the notions of respectfullness+ −
and preservation; Section \ref{sec:lift} describes the lifting of theorems, + −
and Section \ref{sec:conc} concludes and compares our results to existing + −
work.+ −
*}+ −
+ −
section {* Preliminaries and General Quotients\label{sec:prelims} *}+ −
+ −
text {*+ −
We describe in this section briefly the most basic notions of HOL we rely on, and + −
the important definitions given by Homeier for quotients \cite{Homeier05}.+ −
+ −
At its core HOL is based on a simply-typed term language, where types are + −
recorded in Church-style fashion (that means, we can always infer the type of + −
a term and its subterms without any additional information). The grammars+ −
for types and terms are as follows+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}rl@ {\hspace{3mm}}l@ {}}+ −
@{text "\<sigma>, \<tau> ::="} & @{text "\<alpha> | (\<sigma>,\<dots>, \<sigma>) \<kappa>"} & (type variables and type constructors)\\+ −
@{text "t, s ::="} & @{text "x\<^isup>\<sigma> | c\<^isup>\<sigma> | t t | \<lambda>x\<^isup>\<sigma>. t"} & + −
(variables, constants, applications and abstractions)\\+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
We often write just @{text \<kappa>} for @{text "() \<kappa>"}, and use @{text "\<alpha>s"} and+ −
@{text "\<sigma>s"} to stand for collections of type variables and types,+ −
respectively. The type of a term is often made explicit by writing @{text+ −
"t :: \<sigma>"}. HOL includes a type @{typ bool} for booleans and the function + −
type, written @{text "\<sigma> \<Rightarrow> \<tau>"}. HOL also contains+ −
many primitive and defined constants; this includes equality, with type @{text "= :: \<sigma> \<Rightarrow>+ −
\<sigma> \<Rightarrow> bool"}, and the identity function, with type @{text "id :: \<sigma> => \<sigma>"} (the former+ −
being primitive and the latter being defined as @{text+ −
"\<lambda>x\<^sup>\<sigma>. x\<^sup>\<sigma>"}).+ −
+ −
An important point to note is that theorems in HOL can be seen as a subset+ −
of terms that are constructed specially (namely through axioms and prove+ −
rules). As a result we are able to define automatic proof+ −
procedures showing that one theorem implies another by decomposing the term+ −
underlying the first theorem.+ −
+ −
Like Homeier, our work relies on map-functions defined for every type constructor,+ −
like @{text map} for lists. Homeier describes in \cite{Homeier05} map-functions+ −
for products, sums,+ −
options and also the following map for function types+ −
+ −
@{thm [display, indent=10] fun_map_def[no_vars, THEN eq_reflection]}+ −
+ −
\noindent+ −
Using this map-function, we can give the following, equivalent, but more + −
uniform, definition for @{text add} shown in \eqref{adddef}:+ −
+ −
@{text [display, indent=10] "add \<equiv> (Rep_int \<singlearr> Rep_int \<singlearr> Abs_int) add_pair"}+ −
+ −
\noindent+ −
Using extensionality and unfolding the definition, we can get back to \eqref{adddef}. + −
In what follows we shall use the terminology @{text "map_\<kappa>"} for a map-function + −
defined for the type-constructor @{text \<kappa>}. In our implementation we have + −
a database of map-functions that can be dynamically extended.+ −
+ −
It will also be necessary to have operators, referred to as @{text "rel_\<kappa>"},+ −
which define equivalence relations in terms of constituent equivalence+ −
relations. For example given two equivalence relations @{text "R\<^isub>1"}+ −
and @{text "R\<^isub>2"}, we can define an equivalence relations over + −
products as follows+ −
%+ −
@{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"}+ −
+ −
\noindent+ −
Homeier gives also the following operator for defining equivalence + −
relations over function types+ −
%+ −
@{thm [display, indent=10] fun_rel_def[of "R\<^isub>1" "R\<^isub>2", no_vars, THEN eq_reflection]}+ −
+ −
The central definition in Homeier's work \cite{Homeier05} relates equivalence + −
relations, abstraction and representation functions:+ −
+ −
\begin{definition}[Quotient Types]+ −
Given a relation $R$, an abstraction function $Abs$+ −
and a representation function $Rep$, the predicate @{term "Quotient R Abs Rep"}+ −
means+ −
\begin{enumerate}+ −
\item @{thm (rhs1) Quotient_def[of "R", no_vars]}+ −
\item @{thm (rhs2) Quotient_def[of "R", no_vars]}+ −
\item @{thm (rhs3) Quotient_def[of "R", no_vars]}+ −
\end{enumerate}+ −
\end{definition}+ −
+ −
\noindent+ −
The value of this definition is that validity of @{text "Quotient R Abs Rep"} can + −
often be proved in terms of the validity of @{text "Quotient"} over the constituent + −
types of @{text "R"}, @{text Abs} and @{text Rep}. + −
For example Homeier proves the following property for higher-order quotient+ −
types:+ −
+ −
\begin{proposition}\label{funquot}+ −
@{thm[mode=IfThen] fun_quotient[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2" + −
and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]}+ −
\end{proposition}+ −
+ −
\begin{definition}[Respects]+ −
An element @{text "x"} respects a relation @{text "R"} if and only if @{text "R x x"}.+ −
\end{definition}+ −
+ −
\noindent+ −
As a result, Homeier was able to build an automatic prover that can nearly+ −
always discharge a proof obligation involving @{text "Quotient"}. Our quotient+ −
package makes heavy + −
use of this part of Homeier's work including an extension + −
to deal with compositions of equivalence relations defined as follows+ −
+ −
\begin{definition}[Composition of Relations]+ −
@{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate+ −
composition defined by the rule+ −
%+ −
@{thm [mode=Rule, display, indent=10] pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}+ −
\end{definition}+ −
+ −
\noindent+ −
Unfortunately a quotient type theorem, like Proposition \ref{funquot}, for+ −
the composition of any two quotients in not true (it is not even typable in+ −
the HOL type system). However, we can prove useful instances for compatible+ −
containers. We will show such example in Section \ref{sec:resp}.+ −
+ −
+ −
*}+ −
+ −
section {* Quotient Types and Quotient Definitions\label{sec:type} *}+ −
+ −
text {*+ −
The first step in a quotient construction is to take a name for the new+ −
type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},+ −
defined over a raw type, say @{text "\<sigma>"}. The type of the equivalence+ −
relation must be @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of+ −
the quotient type declaration is therefore+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}\hfill\numbered{typedecl}+ −
\end{isabelle}+ −
+ −
\noindent+ −
and a proof that @{text "R"} is indeed an equivalence relation. Two concrete+ −
examples are+ −
+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
\isacommand{quotient\_type}~~@{text "int = nat \<times> nat / \<approx>\<^bsub>nat \<times> nat\<^esub>"}\\+ −
\isacommand{quotient\_type}~~@{text "\<alpha> fset = \<alpha> list / \<approx>\<^bsub>list\<^esub>"}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
which introduce the type of integers and of finite sets using the+ −
equivalence relations @{text "\<approx>\<^bsub>nat \<times> nat\<^esub>"} and @{text+ −
"\<approx>\<^bsub>list\<^esub>"} defined in \eqref{natpairequiv} and+ −
\eqref{listequiv}, respectively (the proofs about being equivalence+ −
relations is omitted). Given this data, we declare for \eqref{typedecl} internally + −
the quotient types as+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\isacommand{typedef}~~@{text "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>x. c = R x}"}+ −
\end{isabelle}+ −
+ −
\noindent+ −
where the right-hand side is the (non-empty) set of equivalence classes of+ −
@{text "R"}. The restriction in this declaration is that the type variables+ −
in the raw type @{text "\<sigma>"} must be included in the type variables @{text+ −
"\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will provide us with the following+ −
abstraction and representation functions + −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
@{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"}+ −
\end{isabelle}+ −
+ −
\noindent + −
As can be seen from the type, they relate the new quotient type and equivalence classes of the raw+ −
type. However, as Homeier \cite{Homeier05} noted, it is much more convenient+ −
to work with the following derived abstraction and representation functions+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
@{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)"}+ −
\end{isabelle}+ −
+ −
\noindent+ −
on the expense of having to use Hilbert's choice operator @{text "\<epsilon>"} in the+ −
definition of @{text "Rep_\<kappa>\<^isub>q"}. These derived notions relate the+ −
quotient type and the raw type directly, as can be seen from their type,+ −
namely @{text "\<sigma> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"},+ −
respectively. Given that @{text "R"} is an equivalence relation, the+ −
following property+ −
+ −
\begin{proposition}+ −
@{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}+ −
\end{proposition}+ −
+ −
\noindent+ −
holds for every quotient type defined+ −
as above (for the proof see \cite{Homeier05}).+ −
+ −
The next step in a quotient construction is to introduce definitions of new constants+ −
involving the quotient type. These definitions need to be given in terms of concepts+ −
of the raw type (remember this is the only way how to extend HOL+ −
with new definitions). For the user the visible part of such definitions is the declaration+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~~\isacommand{is}~~@{text "t :: \<sigma>"}+ −
\end{isabelle}+ −
+ −
\noindent+ −
where @{text t} is the definiens (its type @{text \<sigma>} can always be inferred)+ −
and @{text "c"} is the name of definiendum, whose type @{text "\<tau>"} needs to be+ −
given explicitly (the point is that @{text "\<tau>"} and @{text "\<sigma>"} can only differ + −
in places where a quotient and raw type is involved). Two concrete examples are+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
\isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0::nat, 0::nat)"}\\+ −
\isacommand{quotient\_definition}~~@{text "\<Union> :: (\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}~~%+ −
\isacommand{is}~~@{text "flat"} + −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
The first one declares zero for integers and the second the operator for+ −
building unions of finite sets. + −
+ −
The problem for us is that from such declarations we need to derive proper+ −
definitions using the @{text "Abs"} and @{text "Rep"} functions for the+ −
quotient types involved. The data we rely on is the given quotient type+ −
@{text "\<tau>"} and the raw type @{text "\<sigma>"}. They allow us to define \emph{aggregate+ −
abstraction} and \emph{representation functions} using the functions @{text "ABS (\<sigma>,+ −
\<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses we give below. The idea behind+ −
these two functions is to recursively descend into the raw types @{text \<sigma>} and + −
quotient types @{text \<tau>}, and generate the appropriate+ −
@{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore+ −
we generate just the identity whenever the types are equal. On the ``way'' down,+ −
however we might have to use map-functions to let @{text Abs} and @{text Rep} act+ −
over the appropriate types. The clauses of @{text ABS} and @{text REP} + −
are as follows (where we use the short-hand notation @{text "ABS (\<sigma>s, \<tau>s)"} to mean + −
@{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1)\<dots>ABS (\<sigma>\<^isub>i, \<tau>\<^isub>i)"}; similarly for @{text REP}):+ −
+ −
\begin{center}+ −
\hfill+ −
\begin{tabular}{rcl}+ −
\multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ + −
@{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\+ −
@{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\+ −
\multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\ + −
@{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)"}\\+ −
@{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\\+ −
\multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\ + −
@{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\+ −
@{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\+ −
\multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\+ −
@{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)))"}\\+ −
@{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"}+ −
\end{tabular}\hfill\numbered{ABSREP}+ −
\end{center}+ −
%+ −
\noindent+ −
where in the last two clauses we have that the type @{text "\<alpha>s+ −
\<kappa>\<^isub>q"} is the quotient of the raw type @{text "\<rho>s \<kappa>"} (for example+ −
@{text "int"} and @{text "nat \<times> nat"}, or @{text "\<alpha> fset"} and @{text "\<alpha>+ −
list"}). The quotient construction ensures that the type variables in @{text+ −
"\<rho>s"} must be among the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the+ −
matchers for the @{text "\<alpha>s"} when matching @{text "\<rho>s \<kappa>"} against+ −
@{text "\<sigma>s \<kappa>"}. The+ −
function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw+ −
type as follows:+ −
%+ −
\begin{center}+ −
\begin{tabular}{rcl}+ −
@{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a\<^sup>\<alpha>"}\\+ −
@{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id :: \<kappa> \<Rightarrow> \<kappa>"}\\+ −
@{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\+ −
@{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>as. MAP'(\<sigma>)"} + −
\end{tabular}+ −
\end{center}+ −
%+ −
\noindent+ −
In this definition we rely on the fact that we can interpret type-variables @{text \<alpha>} as + −
term variables @{text a}. In the last clause we build an abstraction over all+ −
term-variables inside map-function generated by the auxiliary function + −
@{text "MAP'"}.+ −
The need of aggregate map-functions can be seen in cases where we build quotients, + −
say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}. + −
In this case @{text MAP} generates the + −
aggregate map-function:+ −
+ −
@{text [display, indent=10] "\<lambda>a b. map_prod (map a) b"}+ −
+ −
\noindent+ −
which we need in order to define the aggregate abstraction and representation + −
functions.+ −
+ −
To see how these definitions pan out in practise, let us return to our+ −
example about @{term "concat"} and @{term "fconcat"}, where we have the raw type+ −
@{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and the quotient type @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>+ −
fset"}. Feeding them into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)+ −
the abstraction function+ −
+ −
@{text [display, indent=10] "(map (map id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map id"}+ −
+ −
\noindent+ −
In our implementation we further+ −
simplify this function by rewriting with the usual laws about @{text+ −
"map"}s and @{text "id"}, namely @{term "map id = id"} and @{text "f \<circ> id =+ −
id \<circ> f = f"}. This gives us the abstraction function+ −
+ −
@{text [display, indent=10] "(map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}+ −
+ −
\noindent+ −
which we can use for defining @{term "fconcat"} as follows+ −
+ −
@{text [display, indent=10] "\<Union> \<equiv> ((map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}+ −
+ −
\noindent+ −
Note that by using the operator @{text "\<singlearr>"} and special clauses+ −
for function types in \eqref{ABSREP}, we do not have to + −
distinguish between arguments and results, but can deal with them uniformly.+ −
Consequently, all definitions in the quotient package + −
are of the general form+ −
+ −
@{text [display, indent=10] "c \<equiv> ABS (\<sigma>, \<tau>) t"}+ −
+ −
\noindent+ −
where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the+ −
type of the defined quotient constant @{text "c"}. This data can be easily+ −
generated from the declaration given by the user.+ −
To increase the confidence in this way of making definitions, we can prove + −
that the terms involved are all typable.+ −
+ −
\begin{lemma}+ −
If @{text "ABS (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"} + −
and @{text "REP (\<sigma>, \<tau>)"} some representation function @{text "Rep"}, + −
then @{text "Abs"} is of type @{text "\<sigma> \<Rightarrow> \<tau>"} and @{text "Rep"} of type+ −
@{text "\<tau> \<Rightarrow> \<sigma>"}.+ −
\end{lemma}+ −
+ −
\begin{proof}+ −
By mutual induction and analysing the definitions of @{text "ABS"}, @{text "REP"}+ −
and @{text "MAP"}. The cases of equal types and function types are+ −
straightforward (the latter follows from @{text "\<singlearr>"} having the+ −
type @{text "(\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> (\<gamma> \<Rightarrow> \<delta>) \<Rightarrow> (\<beta> \<Rightarrow> \<gamma>) \<Rightarrow> (\<alpha> \<Rightarrow> \<delta>)"}). In case of equal type+ −
constructors we can observe that a map-function after applying the functions+ −
@{text "ABS (\<sigma>s, \<tau>s)"} produces a term of type @{text "\<sigma>s \<kappa> \<Rightarrow> \<tau>s \<kappa>"}. The+ −
interesting case is the one with unequal type constructors. Since we know+ −
the quotient is between @{text "\<alpha>s \<kappa>\<^isub>q"} and @{text "\<rho>s \<kappa>"}, we have+ −
that @{text "Abs_\<kappa>\<^isub>q"} is of type @{text "\<rho>s \<kappa> \<Rightarrow> \<alpha>s+ −
\<kappa>\<^isub>q"}. This type can be more specialised to @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s+ −
\<kappa>\<^isub>q"} where the type variables @{text "\<alpha>s"} are instantiated with the+ −
@{text "\<tau>s"}. The complete type can be calculated by observing that @{text+ −
"MAP (\<rho>s \<kappa>)"}, after applying the functions @{text "ABS (\<sigma>s', \<tau>s)"} to it,+ −
returns a term of type @{text "\<rho>s[\<sigma>s'] \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}. This type is+ −
equivalent to @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}, which we just have to compose with+ −
@{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"} according to the type of @{text "\<circ>"}.\qed+ −
\end{proof}+ −
+ −
\noindent+ −
The reader should note that this lemma fails for the abstraction and representation + −
functions used, for example, in Homeier's quotient package.+ −
*}+ −
+ −
section {* Respectfulness and Preservation \label{sec:resp} *}+ −
+ −
text {*+ −
The main point of the quotient package is to automatically ``lift'' theorems+ −
involving constants over the raw type to theorems involving constants over+ −
the quotient type. Before we can describe this lift process, we need to impose + −
some restrictions. The reason is that even if definitions for all raw constants + −
can be given, \emph{not} all theorems can be actually be lifted. Most notably is+ −
the bound variable function, that is the constant @{text bn}, defined for + −
raw lambda-terms as follows+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+ −
@{text "bn (x) \<equiv> \<emptyset>"}\hspace{4mm}+ −
@{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{4mm}+ −
@{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}+ −
\end{isabelle}+ −
+ −
\noindent+ −
This constant just does not respect @{text "\<alpha>"}-equivalence and as+ −
consequently no theorem involving this constant can be lifted to @{text+ −
"\<alpha>"}-equated lambda terms. Homeier formulates the restrictions in terms of+ −
the properties of \emph{respectfullness} and \emph{preservation}. We have+ −
to slightly extend Homeier's definitions in order to deal with quotient+ −
compositions. + −
+ −
To formally define what respectfulness is, we have to first define + −
the notion of \emph{aggregate equivalence relations}.+ −
+ −
TBD+ −
+ −
\begin{itemize}+ −
\item @{text "REL(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "op ="}+ −
\item @{text "REL(\<sigma>, \<sigma>)"} = @{text "op ="}+ −
\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))"}+ −
\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"}+ −
\end{itemize}+ −
+ −
class returned by this constant depends only on the equivalence+ −
classes of the arguments applied to the constant. To automatically+ −
lift a theorem that talks about a raw constant, to a theorem about+ −
the quotient type a respectfulness theorem is required.+ −
+ −
A respectfulness condition for a constant can be expressed in+ −
terms of an aggregate relation between the constant and itself,+ −
for example the respectfullness for @{text "append"}+ −
can be stated as:+ −
+ −
@{text [display, indent=10] "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}+ −
+ −
\noindent+ −
Which after unfolding the definition of @{term "op ===>"} is equivalent to:+ −
+ −
@{thm [display, indent=10] append_rsp_unfolded[no_vars]}+ −
+ −
\noindent An aggregate relation is defined in terms of relation+ −
composition, so we define it first:+ −
+ −
+ −
+ −
The aggregate relation for an aggregate raw type and quotient type+ −
is defined as:+ −
+ −
+ −
Again, the last case is novel, so lets look at the example of+ −
respectfullness for @{term concat}. The statement according to+ −
the definition above is:+ −
+ −
@{thm [display, indent=10] concat_rsp[no_vars]}+ −
+ −
\noindent+ −
By unfolding the definition of relation composition and relation map+ −
we can see the equivalent statement just using the primitive list+ −
equivalence relation:+ −
+ −
@{thm [display, indent=10] concat_rsp_unfolded[of "a" "a'" "b'" "b", no_vars]}+ −
+ −
The statement reads that, for any lists of lists @{term a} and @{term b}+ −
if there exist intermediate lists of lists @{term "a'"} and @{term "b'"}+ −
such that each element of @{term a} is in the relation with an appropriate+ −
element of @{term a'}, @{term a'} is in relation with @{term b'} and each+ −
element of @{term b'} is in relation with the appropriate element of+ −
@{term b}.+ −
+ −
+ −
Sometimes a non-lifted polymorphic constant is instantiated to a+ −
type being lifted. For example take the @{term "op #"} which inserts+ −
an element in a list of pairs of natural numbers. When the theorem+ −
is lifted, the pairs of natural numbers are to become integers, but+ −
the head constant is still supposed to be the head constant, just+ −
with a different type. To be able to lift such theorems+ −
automatically, additional theorems provided by the user are+ −
necessary, we call these \emph{preservation} theorems following+ −
Homeier's naming.+ −
+ −
To lift theorems that talk about insertion in lists of lifted types+ −
we need to know that for any quotient type with the abstraction and+ −
representation functions @{text "Abs"} and @{text Rep} we have:+ −
+ −
@{thm [display, indent=10] (concl) cons_prs[no_vars]}+ −
+ −
This is not enough to lift theorems that talk about quotient compositions.+ −
For some constants (for example empty list) it is possible to show a+ −
general compositional theorem, but for @{term "op #"} it is necessary+ −
to show that it respects the particular quotient type:+ −
+ −
@{thm [display, indent=10] insert_preserve2[no_vars]}+ −
+ −
{\it Composition of Quotient theorems}+ −
+ −
Given two quotients, one of which quotients a container, and the+ −
other quotients the type in the container, we can write the+ −
composition of those quotients. To compose two quotient theorems+ −
we compose the relations with relation composition as defined above+ −
and the abstraction and relation functions are the ones of the sub+ −
quotients composed with the usual function composition.+ −
The @{term "Rep"} and @{term "Abs"} functions that we obtain agree+ −
with the definition of aggregate Abs/Rep functions and the+ −
relation is the same as the one given by aggregate relations.+ −
This becomes especially interesting+ −
when we compose the quotient with itself, as there is no simple+ −
intermediate step.+ −
+ −
Lets take again the example of @{term flat}. To be able to lift+ −
theorems that talk about it we provide the composition quotient+ −
theorem which allows quotienting inside the container:+ −
+ −
If @{term R} is an equivalence relation and @{term "Quotient R Abs Rep"}+ −
then+ −
+ −
@{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)"}+ −
+ −
\noindent+ −
this theorem will then instantiate the quotients needed in the+ −
injection and cleaning proofs allowing the lifting procedure to+ −
proceed in an unchanged way.+ −
+ −
*}+ −
+ −
+ −
section {* Lifting of Theorems\label{sec:lift} *}+ −
+ −
text {*+ −
The core of our quotient package takes an original theorem+ −
involving raw types and a statement of the theorem that+ −
it is supposed to produce. This is different from existing+ −
quotient packages, where only the raw theorems are necessary.+ −
To simplify the use of the quotient package we additionally provide+ −
an automated statement translation mechanism which can produce+ −
the latter automatically given a list of quotient types.+ −
It is possible that a user wants+ −
to lift only some occurrences of a raw type. In this case+ −
the user specifies the complete lifted goal instead of using the+ −
automated mechanism.+ −
Lifting the theorems is performed in three steps. In the following+ −
we call these steps \emph{regularization}, \emph{injection} and+ −
\emph{cleaning} following the names used in Homeier's HOL4+ −
implementation.+ −
+ −
We first define the statement of the regularized theorem based+ −
on the original theorem and the goal theorem. Then we define+ −
the statement of the injected theorem, based on the regularized+ −
theorem and the goal. We then show the 3 proofs, as all three+ −
can be performed independently from each other.+ −
+ −
*}+ −
text {* \textit{Regularization and Injection statements} *}+ −
text {*+ −
+ −
We define the function @{text REG}, which takes the statements+ −
of the raw theorem and the lifted theorem (both as terms) and+ −
returns the statement of the regularized version. The intuition+ −
behind this function is that it replaces quantifiers and+ −
abstractions involving raw types by bounded ones, and equalities+ −
involving raw types are replaced by appropriate aggregate+ −
equivalence relations. It is defined as follows:+ −
+ −
\begin{center}+ −
\begin{tabular}{rcl}+ −
\multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\+ −
@{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma>. REG (t, s)"}\\+ −
@{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}\\+ −
\multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\+ −
@{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma>. REG (t, s)"}\\+ −
@{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}\\+ −
\multicolumn{3}{@ {\hspace{-4mm}}l}{equalities (with same types and different types):}\\+ −
@{text "REG ((op =) : \<sigma>, (op =) : \<sigma>)"} & $\dn$ & @{text "(op =) : \<sigma>"}\\+ −
@{text "REG ((op =) : \<sigma>, (op =) : \<tau>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>) : \<sigma>"}\\+ −
\multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables, constants:}\\+ −
@{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)"}\\+ −
@{text "REG (v\<^isub>1, v\<^isub>2)"} & $\dn$ & @{text "v\<^isub>1"}\\+ −
@{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
In the above definition we omitted the cases for existential quantifiers+ −
and unique existential quantifiers, as they are very similar to the cases+ −
for the universal quantifier.+ −
Next we define the function @{text INJ} which takes the statement of+ −
the regularized theorems and the statement of the lifted theorem both as+ −
terms and returns the statement of the injected theorem:+ −
+ −
\begin{center}+ −
\begin{tabular}{rcl}+ −
\multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\+ −
@{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) "} & $\dn$ & @{text "\<lambda>x. INJ (t, s)"}\\+ −
@{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"}\\+ −
@{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))))"}\\+ −
\multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\+ −
@{text "INJ (\<forall> t, \<forall> s) "} & $\dn$ & @{text "\<forall> (INJ (t, s))"}\\+ −
@{text "INJ (\<forall> t \<in> R, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s) \<in> R"}\\+ −
\multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables, constants:}\\+ −
@{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)"}\\+ −
@{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) "} & $\dn$ & @{text "v\<^isub>1"}\\+ −
@{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"}\\+ −
@{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) "} & $\dn$ & @{text "c\<^isub>1"}\\+ −
@{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
For existential quantifiers and unique existential quantifiers it is+ −
defined similarly to the universal one.+ −
+ −
*}+ −
text {*\textit{Proof Procedure}*}+ −
+ −
(* In the below the type-guiding 'QuotTrue' assumption is removed. We need it+ −
only for bound variables without types, while in the paper presentation+ −
variables are typed *)+ −
+ −
text {*+ −
+ −
When lifting a theorem we first apply the following rule+ −
+ −
@{term [display, indent=10] "[|A; A --> B; B = C; C = D|] ==> D"}+ −
+ −
\noindent+ −
with @{text A} instantiated to the original raw theorem, + −
@{text B} instantiated to @{text "REG(A)"},+ −
@{text C} instantiated to @{text "INJ(REG(A))"},+ −
and @{text D} instantiated to the statement of the lifted theorem.+ −
The first assumption can be immediately discharged using the original+ −
theorem and the three left subgoals are exactly the subgoals of regularization,+ −
injection and cleaning. The three can be proved independently by the+ −
framework and in case there are non-solved subgoals they can be left+ −
to the user.+ −
+ −
The injection and cleaning subgoals are always solved if the appropriate+ −
respectfulness and preservation theorems are given. It is not the case+ −
with regularization; sometimes a theorem given by the user does not+ −
imply a regularized version and a stronger one needs to be proved. This+ −
is outside of the scope of the quotient package, so such obligations are+ −
left to the user. Take a simple statement for integers @{term "0 \<noteq> 1"}.+ −
It does not follow from the fact that @{term "\<not> (0, 0) = (1, 0)"} because+ −
of regularization. The raw theorem only shows that particular items in the+ −
equivalence classes are not equal. A more general statement saying that+ −
the classes are not equal is necessary.+ −
+ −
*}+ −
text {* \textit{Proving Regularization} *}+ −
text {*+ −
+ −
Isabelle provides a set of \emph{mono} rules, that are used to split implications+ −
of similar statements into simpler implication subgoals. These are enhanced+ −
with special quotient theorem in the regularization proof. Below we only show+ −
the versions for the universal quantifier. For the existential quantifier+ −
and abstraction they are analogous.+ −
+ −
First, bounded universal quantifiers can be removed on the right:+ −
+ −
@{thm [display, indent=10] ball_reg_right_unfolded[no_vars]}+ −
+ −
They can be removed anywhere if the relation is an equivalence relation:+ −
+ −
@{thm [display, indent=10] (concl) ball_reg_eqv[no_vars]}+ −
+ −
And finally it can be removed anywhere if @{term R2} is an equivalence relation:+ −
+ −
@{thm [display, indent=10] (concl) ball_reg_eqv_range[no_vars]}+ −
+ −
The last theorem is new in comparison with Homeier's package. There the+ −
injection procedure would be used to prove goals with such shape, and there+ −
the equivalence assumption would be used. We use the above theorem directly+ −
also for composed relations where the range type is a type for which we know an+ −
equivalence theorem. This allows separating regularization from injection.+ −
*}+ −
text {* \textit{Proving Rep/Abs Injection} *}+ −
+ −
(*+ −
@{thm bex_reg_eqv_range[no_vars]}+ −
@{thm [display] bex_reg_left[no_vars]}+ −
@{thm [display] bex1_bexeq_reg[no_vars]}+ −
@{thm [display] bex_reg_eqv[no_vars]}+ −
@{thm [display] babs_reg_eqv[no_vars]}+ −
@{thm [display] babs_simp[no_vars]}+ −
*)+ −
+ −
text {*+ −
The injection proof starts with an equality between the regularized theorem+ −
and the injected version. The proof again follows by the structure of the+ −
two terms, and is defined for a goal being a relation between these two terms.+ −
+ −
\begin{itemize}+ −
\item For two constants, an appropriate constant respectfullness assumption is used.+ −
\item For two variables, we use the assumptions proved in regularization.+ −
\item For two abstractions, they are eta-expanded and beta-reduced.+ −
\end{itemize}+ −
+ −
Otherwise the two terms are applications. There are two cases: If there is a REP/ABS+ −
in the injected theorem we can use the theorem:+ −
+ −
@{thm [display, indent=10] rep_abs_rsp[no_vars]}+ −
+ −
\noindent+ −
and continue the proof.+ −
+ −
Otherwise we introduce an appropriate relation between the subterms and continue with+ −
two subgoals using the lemma:+ −
+ −
@{thm [display, indent=10] apply_rsp[no_vars]}+ −
+ −
*}+ −
text {* \textit{Cleaning} *}+ −
text {*+ −
+ −
The @{text REG} and @{text INJ} functions have been defined in such a way+ −
that establishing the goal theorem now consists only on rewriting the+ −
injected theorem with the preservation theorems.+ −
+ −
\begin{itemize}+ −
\item First for lifted constants, their definitions are the preservation rules for+ −
them.+ −
\item For lambda abstractions lambda preservation establishes+ −
the equality between the injected theorem and the goal. This allows both+ −
abstraction and quantification over lifted types.+ −
@{thm [display] (concl) lambda_prs[no_vars]}+ −
\item Relations over lifted types are folded with:+ −
@{thm [display] (concl) Quotient_rel_rep[no_vars]}+ −
\item User given preservation theorems, that allow using higher level operations+ −
and containers of types being lifted. An example may be+ −
@{thm [display] (concl) map_prs(1)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]}+ −
\end{itemize}+ −
+ −
*}+ −
+ −
section {* Examples *}+ −
+ −
(* Mention why equivalence *)+ −
+ −
text {*+ −
+ −
In this section we will show, a complete interaction with the quotient package+ −
for defining the type of integers by quotienting pairs of natural numbers and+ −
lifting theorems to integers. Our quotient package is fully compatible with+ −
Isabelle type classes, but for clarity we will not use them in this example.+ −
In a larger formalization of integers using the type class mechanism would+ −
provide many algebraic properties ``for free''.+ −
+ −
A user of our quotient package first needs to define a relation on+ −
the raw type, by which the quotienting will be performed. We give+ −
the same integer relation as the one presented in the introduction:+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %+ −
\isacommand{fun}~~@{text "int_rel"}~~\isacommand{where}~~@{text "(m \<Colon> nat, n) int_rel (p, q) = (m + q = n + p)"}+ −
\end{isabelle}+ −
+ −
\noindent+ −
Next the quotient type is defined. This leaves a proof obligation that the+ −
relation is an equivalence relation which is solved automatically using the+ −
definitions:+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %+ −
\isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"}+ −
\end{isabelle}+ −
+ −
\noindent+ −
The user can then specify the constants on the quotient type:+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %+ −
\begin{tabular}{@ {}l}+ −
\isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0::nat, 0::nat)"}\\+ −
\isacommand{fun}~~@{text "plus_raw"}~~\isacommand{where}~~@{text "plus_raw (m :: nat, n) (p, q) = (m + p, n + q)"}\\+ −
\isacommand{quotient\_definition}~~@{text "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)"}~~\isacommand{is}~~@{text "plus_raw"}\\+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
Lets first take a simple theorem about addition on the raw level:+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %+ −
\isacommand{lemma}~~@{text "plus_zero_raw: int_rel (plus_raw (0, 0) x) x"}+ −
\end{isabelle}+ −
+ −
\noindent+ −
When the user tries to lift a theorem about integer addition, the respectfulness+ −
proof obligation is left, so let us prove it first:+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %+ −
\isacommand{lemma}~~@{text "[quot_respect]: (int_rel \<Longrightarrow> int_rel \<Longrightarrow> int_rel) plus_raw plus_raw"}+ −
\end{isabelle}+ −
+ −
\noindent+ −
Can be proved automatically by the system just by unfolding the definition+ −
of @{text "op \<Longrightarrow>"}.+ −
Now the user can either prove a lifted lemma explicitly:+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %+ −
\isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting plus_zero_raw"}+ −
\end{isabelle}+ −
+ −
\noindent+ −
Or in this simple case use the automated translation mechanism:+ −
+ −
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %+ −
\isacommand{thm}~~@{text "plus_zero_raw[quot_lifted]"}+ −
\end{isabelle}+ −
+ −
\noindent+ −
obtaining the same result.+ −
*}+ −
+ −
section {* Conclusion and Related Work\label{sec:conc}*}+ −
+ −
text {*+ −
+ −
The code of the quotient package and the examples described here are+ −
already included in the+ −
standard distribution of Isabelle.\footnote{Available from+ −
\href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is+ −
heavily used in Nominal Isabelle, which provides a convenient reasoning+ −
infrastructure for programming language calculi involving binders. Earlier+ −
versions of Nominal Isabelle have been used successfully in formalisations+ −
of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08},+ −
Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for+ −
concurrency \cite{BengtsonParow09} and a strong normalisation result for+ −
cut-elimination in classical logic \cite{UrbanZhu08}.+ −
+ −
Oscar Slotosch~\cite{Slotosch97} implemented a mechanism that automatically+ −
defines quotient types for Isabelle/HOL. It did not include theorem lifting.+ −
John Harrison's quotient package~\cite{harrison-thesis} is the first one to+ −
lift theorems, however only first order. There is work on quotient types in+ −
non-HOL based systems and logical frameworks, namely theory interpretations+ −
in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or+ −
the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}.+ −
Larry Paulson shows a construction of quotients that does not require the+ −
Hilbert Choice operator, again only first order~\cite{Paulson06}.+ −
The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05},+ −
which is the first one to support lifting of higher order theorems.+ −
+ −
+ −
Our quotient package for the first time explore the notion of+ −
composition of quotients, which allows lifting constants like @{term+ −
"concat"} and theorems about it. We defined the composition of+ −
relations and showed examples of compositions of quotients which+ −
allows lifting polymorphic types with subtypes quotiented as well.+ −
We extended the notions of respectfullness and preservation;+ −
with quotient compositions there is more than one condition needed+ −
for a constant.+ −
+ −
Our package is modularized, so that single definitions, single+ −
theorems or single respectfullness conditions etc can be added,+ −
which allows the use of the quotient package together with+ −
type-classes and locales. This has the advantage over packages+ −
requiring big lists as input for the user of being able to develop+ −
a theory progressively.+ −
+ −
We allow lifting only some occurrences of quotiented types, which+ −
is useful in Nominal. The package can be used automatically with+ −
an attribute, manually with separate tactics for parts of the lifting+ −
procedure, and programatically. Automated definitions of constants+ −
and respectfulness proof obligations are used in Nominal. Finally+ −
we streamlined and showed the detailed lifting procedure, which+ −
has not been presented before.+ −
+ −
\medskip+ −
\noindent+ −
{\bf Acknowledgements:} We would like to thank Peter Homeier for the+ −
discussions about the HOL4 quotient package and explaining us its+ −
implementation details.+ −
+ −
*}+ −
+ −
+ −
+ −
(*<*)+ −
end+ −
(*>*)+ −