(* How to change the notation for \<lbrakk> \<rbrakk> meta-level implications? *)+ −
+ −
(*<*)+ −
theory Paper+ −
imports "Quotient"+ −
"LaTeXsugar"+ −
"../Nominal/FSet"+ −
begin+ −
+ −
notation (latex output)+ −
rel_conj ("_ OOO _" [53, 53] 52) and+ −
"op -->" (infix "\<rightarrow>" 100) and+ −
"==>" (infix "\<Rightarrow>" 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}\smallskip+ −
+ −
\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+ −
+ −
@{text [display, indent=10] "(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"}+ −
+ −
\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+ −
+ −
@{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}+ −
+ −
\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.+ −
+ −
An area where quotients are ubiquitous is reasoning about programming language+ −
calculi. A simple example is the lambda-calculus, whose raw terms are defined as+ −
+ −
@{text [display, indent=10] "t ::= x | t t | \<lambda>x.t"}+ −
+ −
\noindent+ −
The problem with this definition arises when one attempts to+ −
prove formally, for example, 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 to 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 definitions and 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 is the one 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, often referred to as the+ −
\emph{raw level}, 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 level}. This type comes with an+ −
\emph{abstraction} and a \emph{representation} function, written @{text Abs}+ −
and @{text Rep}. These functions relate elements in the existing type to+ −
ones in the new type and vice versa; they can be uniquely identified by+ −
their 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+ −
However we often leave this typing information implicit for better+ −
readability. 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 (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs (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+ −
+ −
@{text [display, indent=10] "add n m \<equiv> Abs (add_pair (Rep n) (Rep m))"}+ −
+ −
\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 obtain 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"},+ −
behaves as follows:+ −
+ −
@{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}+ −
+ −
\noindent+ −
The quotient package should provide us with a definition for @{text "\<Union>"} in+ −
terms of @{text flat}, @{text Rep} and @{text Abs} (the latter two having+ −
the type @{text "\<alpha> fset \<Rightarrow> \<alpha> list"} and @{text "\<alpha> list \<Rightarrow> \<alpha> fset"},+ −
respectively). The problem is that the method used in the existing quotient+ −
packages of just taking the representation of the arguments and then take+ −
the abstraction of the result is \emph{not} enough. The reason is that case in case+ −
of @{text "\<Union>"} we obtain the incorrect definition+ −
+ −
@{text [display, indent=10] "\<Union> S \<equiv> Abs (flat (Rep 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 (flat ((map Rep \<circ> Rep) 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{respectfulness} and \emph{preservation} from Homeier + −
\cite{Homeier05}.+ −
+ −
We will also 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. 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 to develop a formal theory interactively an a natural progression. A+ −
pleasing result of the modularity is also that we are able to clearly+ −
specify what needs to be done 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 \ldots+ −
*}+ −
+ −
+ −
+ −
section {* Preliminaries and General Quotient\label{sec:prelims} *}+ −
+ −
+ −
+ −
text {*+ −
In this section we present the definitions of a quotient that follow+ −
those by Homeier, the proofs can be found there.+ −
+ −
\begin{definition}[Quotient]+ −
A relation $R$ with an abstraction function $Abs$+ −
and a representation function $Rep$ is a \emph{quotient}+ −
if and only if:+ −
+ −
\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}+ −
+ −
\begin{definition}[Relation map and function map]\\+ −
@{thm fun_rel_def[of "R1" "R2", no_vars]}\\+ −
@{thm fun_map_def[no_vars]}+ −
\end{definition}+ −
+ −
The main theorems for building higher order quotients is:+ −
\begin{lemma}[Function Quotient]+ −
If @{thm (prem 1) fun_quotient[no_vars]} and @{thm (prem 2) fun_quotient[no_vars]}+ −
then @{thm (concl) fun_quotient[no_vars]}+ −
\end{lemma}+ −
+ −
*}+ −
+ −
subsection {* Higher Order Logic *}+ −
+ −
text {*+ −
+ −
Types:+ −
\begin{eqnarray}\nonumber+ −
@{text "\<sigma> ::="} & @{text "\<alpha>"} & \textrm{(type variable)} \\ \nonumber+ −
@{text "|"} & @{text "(\<sigma>,\<dots>,\<sigma>)\<kappa>"} & \textrm{(type construction)}+ −
\end{eqnarray}+ −
+ −
Terms:+ −
\begin{eqnarray}\nonumber+ −
@{text "t ::="} & @{text "x\<^isup>\<sigma>"} & \textrm{(variable)} \\ \nonumber+ −
@{text "|"} & @{text "c\<^isup>\<sigma>"} & \textrm{(constant)} \\ \nonumber+ −
@{text "|"} & @{text "t t"} & \textrm{(application)} \\ \nonumber+ −
@{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber+ −
\end{eqnarray}+ −
+ −
*}+ −
+ −
section {* Quotient Types and Lifting of Definitions *}+ −
+ −
(* Say more about containers? *)+ −
+ −
text {*+ −
+ −
To define a constant on the lifted type, an aggregate abstraction+ −
function is applied to the raw constant. Below we describe the operation+ −
that generates+ −
an aggregate @{term "Abs"} or @{term "Rep"} function given the+ −
compound raw type and the compound quotient type.+ −
This operation will also be used in translations of theorem statements+ −
and in the lifting procedure.+ −
+ −
The operation is additionally able to descend into types for which+ −
maps are known. Such maps for most common types (list, pair, sum,+ −
option, \ldots) are described in Homeier, and we assume that @{text "map"}+ −
is the function that returns a map for a given type. Then REP/ABS is defined+ −
as follows:+ −
+ −
{\it the first argument is the raw type and the second argument the quotient type}+ −
+ −
+ −
\begin{center}+ −
\begin{tabular}{rcl}+ −
+ −
% type variable case says that variables must be equal...therefore subsumed by the equal case below+ −
%+ −
%\multicolumn{3}{@ {\hspace{-4mm}}l}{type variables:}\\ + −
%@{text "ABS (\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} & $\dn$ & @{text "id"}\\+ −
%@{text "REP (\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} & $\dn$ & @{text "id"}\smallskip\\+ −
+ −
\multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ + −
@{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\\+ −
@{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\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 "\<kappa>_map (ABS (\<sigma>s, \<tau>s))"}\\+ −
@{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "\<kappa>_map (REP (\<sigma>s, \<tau>s))"}\smallskip\\+ −
\multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\+ −
@{text "ABS (\<sigma>s \<kappa>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "\<kappa>\<^isub>2_Abs \<circ> \<kappa>\<^isub>1_map (ABS (\<sigma>s', \<tau>s'))"}\\+ −
@{text "REP (\<sigma>s \<kappa>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "\<kappa>\<^isub>1_map (REP (\<sigma>s', \<tau>s')) \<circ> \<kappa>\<^isub>2_Rep"}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
\begin{center}+ −
\begin{tabular}{rcl}+ −
@{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n) \<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m) \<kappa>\<^isub>2)"} = @{text "Abs_\<kappa>\<^isub>2 \<circ> (map \<kappa>\<^isub>1) (ABS(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (ABS(\<rho>\<^isub>p,\<nu>\<^isub>p)"}\\ + −
@{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n) \<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m) \<kappa>\<^isub>2)"} = @{text "(map \<kappa>\<^isub>1) (REP(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REP(\<rho>\<^isub>p,\<nu>\<^isub>p) \<circ> Rep_\<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{tabular}+ −
\end{center}+ −
+ −
Apart from the last 2 points the definition is same as the one implemented in+ −
in Homeier's HOL package. Adding composition in last two cases is necessary+ −
for compositional quotients. We ilustrate the different behaviour of the+ −
definition by showing the derived definition of @{term fconcat}:+ −
+ −
@{thm fconcat_def[no_vars]}+ −
+ −
The aggregate @{term Abs} function takes a finite set of finite sets+ −
and applies @{term "map rep_fset"} composed with @{term rep_fset} to+ −
its input, obtaining a list of lists, passes the result to @{term concat}+ −
obtaining a list and applies @{term abs_fset} obtaining the composed+ −
finite set.+ −
+ −
{\it we can compactify the term by noticing that map id\ldots id = id}+ −
+ −
{\it we should be able to prove}+ −
+ −
\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}+ −
*}+ −
+ −
subsection {* Respectfulness *}+ −
+ −
text {*+ −
+ −
A respectfulness lemma for a constant states that the equivalence+ −
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 @{term "append"}+ −
can be stated as:+ −
+ −
@{thm [display, indent=10] append_rsp[no_vars]}+ −
+ −
\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:+ −
+ −
\begin{definition}[Composition of Relations]+ −
@{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate+ −
composition @{thm pred_compI[no_vars]}+ −
\end{definition}+ −
+ −
The aggregate relation for an aggregate raw type and quotient type+ −
is defined as:+ −
+ −
\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}+ −
+ −
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}.+ −
+ −
*}+ −
+ −
subsection {* Preservation *}+ −
+ −
text {*+ −
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]}+ −
*}+ −
+ −
subsection {* Composition of Quotient theorems *}+ −
+ −
text {*+ −
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 concat}. To be able to lift+ −
theorems that talk about it we provide the composition quotient+ −
theorems, which then lets us perform the lifting procedure in an+ −
unchanged way:+ −
+ −
@{thm [display] quotient_compose_list[no_vars]}+ −
*}+ −
+ −
+ −
section {* Lifting of Theorems *}+ −
+ −
text {*+ −
The core of the quotient package takes an original theorem that+ −
talks about the raw types, and the statement of the theorem that+ −
it is supposed to produce. This is different from other existing+ −
quotient packages, where only the raw theorems were necessary.+ −
We notice that in some cases only some occurrences of the raw+ −
types need to be lifted. This is for example the case in the+ −
new Nominal package, where a raw datatype that talks about+ −
pairs of natural numbers or strings (being lists of characters)+ −
should not be changed to a quotient datatype with constructors+ −
taking integers or finite sets of characters. To simplify the+ −
use of the quotient package we additionally provide an automated+ −
statement translation mechanism that replaces occurrences of+ −
types that match given quotients by appropriate lifted types.+ −
+ −
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 HOL+ −
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.+ −
+ −
*}+ −
+ −
subsection {* Regularization and Injection statements *}+ −
+ −
text {*+ −
+ −
We first 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+ −
relations. It is defined as follows:+ −
+ −
\begin{itemize}+ −
\item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"}+ −
\item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}+ −
\item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"}+ −
\item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}+ −
\item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"}+ −
\item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"}+ −
\item @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}+ −
\item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"}+ −
\item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"}+ −
\end{itemize}+ −
+ −
In the above definition we ommited 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 statment of the injected theorem:+ −
+ −
\begin{itemize}+ −
\item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"}+ −
\item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"}+ −
\item @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"}+ −
\item @{text "INJ (\<forall> t, \<forall> s) = \<forall> (INJ (t, s)"}+ −
\item @{text "INJ (\<forall> t \<in> R, \<forall> s) = \<forall> (INJ (t, s) \<in> R"}+ −
\item @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}+ −
\item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) = v\<^isub>1"}+ −
\item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"}+ −
\item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) = c\<^isub>1"}+ −
\item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"}+ −
\end{itemize}+ −
+ −
For existential quantifiers and unique existential quantifiers it is+ −
defined similarily to the universal one.+ −
+ −
*}+ −
+ −
subsection {* Proof procedure *}+ −
+ −
(* In the below the type-guiding 'QuotTrue' assumption is removed; since we+ −
present in a paper a version with typed-variables it is not necessary *)+ −
+ −
text {*+ −
+ −
With the above definitions of @{text "REG"} and @{text "INJ"} we can show+ −
how the proof is performed. The first step is always the application of+ −
of the following lemma:+ −
+ −
@{term "[|A; A --> B; B = C; C = D|] ==> D"}+ −
+ −
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 the user is then left+ −
with such obligations. As an example lets see the simplest possible+ −
non-liftable theorem for integers: When we want to prove @{term "0 \<noteq> 1"}+ −
on integers the fact that @{term "\<not> (0, 0) = (1, 0)"} is not enough. It+ −
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.+ −
*}+ −
+ −
subsection {* 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 enchanced+ −
with special quotient theorem in the regularization goal. Below we only show+ −
the versions for the universal quantifier. For the existential quantifier+ −
and abstraction they are analoguous with some symmetry.+ −
+ −
First, bounded universal quantifiers can be removed on the right:+ −
+ −
@{thm [display] ball_reg_right[no_vars]}+ −
+ −
They can be removed anywhere if the relation is an equivalence relation:+ −
+ −
@{thm [display] ball_reg_eqv[no_vars]}+ −
+ −
And finally it can be removed anywhere if @{term R2} is an equivalence relation, then:+ −
\[+ −
@{thm (rhs) ball_reg_eqv_range[no_vars]} = @{thm (lhs) ball_reg_eqv_range[no_vars]}+ −
\]+ −
+ −
The last theorem is new in comparison with Homeier's package; it allows separating+ −
regularization from injection.+ −
+ −
*}+ −
+ −
(*+ −
@{thm (rhs) bex_reg_eqv_range[no_vars]} = @{thm (lhs) 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]}+ −
*)+ −
+ −
subsection {* Injection *}+ −
+ −
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 term, and is defined for a goal being a relation between the two terms.+ −
+ −
\begin{itemize}+ −
\item For two constants, an appropriate constant respectfullness assumption is used.+ −
\item For two variables, the regularization assumptions state that they are related.+ −
\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] rep_abs_rsp[no_vars]}+ −
+ −
and continue the proof.+ −
+ −
Otherwise we introduce an appropriate relation between the subterms and continue with+ −
two subgoals using the lemma:+ −
+ −
@{thm [display] apply_rsp[no_vars]}+ −
+ −
*}+ −
+ −
subsection {* 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] lambda_prs[no_vars]}+ −
\item Relations over lifted types are folded with:+ −
@{thm [display] 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] map_prs(1)[no_vars]}+ −
\end{itemize}+ −
+ −
Preservation of relations and user given constant preservation lemmas *}+ −
+ −
section {* Examples *}+ −
+ −
(* Mention why equivalence *)+ −
+ −
text {*+ −
+ −
A user of our quotient package first needs to define an equivalence relation:+ −
+ −
@{text "fun \<approx> where (x, y) \<approx> (u, v) = (x + v = u + y)"}+ −
+ −
Then the user defines a quotient type:+ −
+ −
@{text "quotient_type int = (nat \<times> nat) / \<approx>"}+ −
+ −
Which leaves a proof obligation that the relation is an equivalence relation,+ −
that can be solved with the automatic tactic with two definitions.+ −
+ −
The user can then specify the constants on the quotient type:+ −
+ −
@{text "quotient_definition 0 \<Colon> int is (0\<Colon>nat, 0\<Colon>nat)"}+ −
@{text "fun plus_raw where plus_raw (x, y) (u, v) = (x + u, y + v)"}+ −
@{text "quotient_definition (op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int) is plus_raw"}+ −
+ −
Lets first take a simple theorem about addition on the raw level:+ −
+ −
@{text "lemma plus_zero_raw: plus_raw (0, 0) i \<approx> i"}+ −
+ −
When the user tries to lift a theorem about integer addition, the respectfulness+ −
proof obligation is left, so let us prove it first:+ −
+ −
@{text "lemma (op \<approx> \<Longrightarrow> op \<approx> \<Longrightarrow> op \<approx>) plus_raw plus_raw"}+ −
+ −
Can be proved automatically by the system just by unfolding the definition+ −
of @{term "op \<Longrightarrow>"}.+ −
+ −
Now the user can either prove a lifted lemma explicitely:+ −
+ −
@{text "lemma 0 + i = i by lifting plus_zero_raw"}+ −
+ −
Or in this simple case use the automated translation mechanism:+ −
+ −
@{text "thm plus_zero_raw[quot_lifted]"}+ −
+ −
obtaining the same result.+ −
*}+ −
+ −
section {* Related Work *}+ −
+ −
text {*+ −
\begin{itemize}+ −
+ −
\item Peter Homeier's package~\cite{Homeier05} (and related work from there)+ −
\item John Harrison's one~\cite{harrison-thesis} is the first one to lift theorems+ −
but only first order.+ −
+ −
\item PVS~\cite{PVS:Interpretations}+ −
\item MetaPRL~\cite{Nogin02}+ −
\item Manually defined quotients in Isabelle/HOL Library (Markus's Quotient\_Type,+ −
Dixon's FSet, \ldots)+ −
+ −
\item Oscar Slotosch defines quotient-type automatically but no+ −
lifting~\cite{Slotosch97}.+ −
+ −
\item PER. And how to avoid it.+ −
+ −
\item Necessity of Hilbert Choice op and Larry's quotients~\cite{Paulson06}+ −
+ −
\item Setoids in Coq and \cite{ChicliPS02}+ −
+ −
\end{itemize}+ −
*}+ −
+ −
section {* Conclusion *}+ −
+ −
text {*+ −
The package is part of the standard distribution of Isabelle.+ −
*}+ −
+ −
+ −
subsection {* Contributions *}+ −
+ −
text {*+ −
We present the detailed lifting procedure, which was not shown before.+ −
+ −
The quotient package presented in this paper has the following+ −
advantages over existing packages:+ −
\begin{itemize}+ −
+ −
\item We define quotient composition, function map composition and+ −
relation map composition. This lets lifting polymorphic types with+ −
subtypes quotiented as well. We extend the notions of+ −
respectfulness and preservation to cope with quotient+ −
composition.+ −
+ −
\item We allow lifting only some occurrences of quotiented+ −
types. Rsp/Prs extended. (used in nominal)+ −
+ −
\item The quotient package is very modular. Definitions can be added+ −
separately, rsp and prs can be proved separately, Quotients and maps+ −
can be defined separately and theorems can+ −
be lifted on a need basis. (useful with type-classes).+ −
+ −
\item Can be used both manually (attribute, separate tactics,+ −
rsp/prs databases) and programatically (automated definition of+ −
lifted constants, the rsp proof obligations and theorem statement+ −
translation according to given quotients).+ −
+ −
\end{itemize}+ −
*}+ −
+ −
+ −
+ −
(*<*)+ −
end+ −
(*>*)+ −