(*<*)
theory Paper
imports "Quotient"
"~~/src/HOL/Library/Quotient_Syntax"
"~~/src/HOL/Library/LaTeXsugar"
"~~/src/HOL/Quotient_Examples/FSet"
begin
notation (latex output)
rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
implies (infix "\<longrightarrow>" 100) and
"==>" (infix "\<Longrightarrow>" 100) and
map_fun ("_ \<singlearr> _" 51) and
fun_rel ("_ \<doublearr> _" 51) and
list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
empty_fset ("\<emptyset>") and
union_fset ("_ \<union> _") and
insert_fset ("{_} \<union> _") and
Cons ("_::_") and
concat ("flat") and
concat_fset ("\<Union>") and
Quotient ("Quot _ _ _")
declare [[show_question_marks = false]]
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 (Proof_Context.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))
*}
fun add_pair :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
where "add_pair (n1, m1) (n2, m2) = (n1 + n2, m1 + m2)"
fun minus_pair :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
where "minus_pair (n, m) = (m, n)"
fun
intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" ("_ \<approx> _" [50, 50] 50)
where
"intrel (x, y) (u, v) = (x + v = u + y)"
(*>*)
section {* Introduction *}
text {*
\noindent
One might think quotients have been studied to death, but in the
context of theorem provers a number questions concerning them are
far from settled. In this paper we address the question of how to
establish a convenient reasoning infrastructure for quotient
constructions in the Isabelle/HOL theorem prover. Higher-Order Logic
(HOL) 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. Previous work has shown 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:
\begin{isabelle}\ \ \ \ \ %%%
@{thm add_pair.simps[where ?n1.0="n\<^isub>1" and ?n2.0="n\<^isub>2" and ?m1.0="m\<^isub>1" and ?m2.0="m\<^isub>2", THEN eq_reflection]}%
\hfill\numbered{addpair}
\end{isabelle}
\noindent
Negation on integers is defined in terms of swapping of pairs:
\begin{isabelle}\ \ \ \ \ %%%
@{thm minus_pair.simps[where ?n="n" and ?m="m", THEN eq_reflection]}%
\hfill\numbered{minuspair}
\end{isabelle}
\noindent
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, and vice versa. 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, or un-quotient, 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 from the need to reason
modulo $\alpha$-equivalence, 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 fundamental reason is that in case of
$\alpha$-equated terms, equality coincides with $\alpha$-equivalence and
we can use for reasoning HOL's built-in notion of ``replacing equals by equals''.
There is also often a need to consider quotients of parial equivalence relations. For
example the rational numbers
can be constructed using pairs of integers and the partial 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{ratpairequiv}
\end{isabelle}
\noindent
where @{text "n\<^isub>2"} and @{text "m\<^isub>2"} are not allowed to be zero.
The difficulty is that in order to be able to reason about integers,
finite sets, etc.~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, $\alpha$-equated lambda-terms and
rational numbers). This lifting usually requires a reasoning effort
that can be rather repetitive and involves explicit conversions
between the quotient and raw level in form of abstraction and
representation functions \cite{Paulson06}. In principle 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. Before we
delve into the details, let us show how the user interacts with our
quotient package when defining integers. We assume the definitions
involving pairs of natural numbers shown in \eqref{natpairequiv},
\eqref{addpair} and \eqref{minuspair} have already been made. A
quotient can then be introduced by declaring the new type (in this case
@{typ int}), the raw type (that is @{typ "nat \<times> nat"}) and the
equivalence relation (that is @{text intrel} defined in
\eqref{natpairequiv}).
*}
quotient_type int = "nat \<times> nat" / intrel
txt {*
\noindent
This declaration requires the user to prove that @{text intrel} is
indeed an equivalence relation, whereby an equivalence
relation is defined as one that is reflexive, symmetric and
transitive. This proof obligation can thus be discharged by
unfolding the definitions and using the standard automatic proving
tactic in Isabelle/HOL.
*}
unfolding equivp_reflp_symp_transp
unfolding reflp_def symp_def transp_def
by auto
(*<*)
instantiation int :: "{zero, one, plus, uminus}"
begin
(*>*)
text {*
\noindent
Next we can declare the constants @{text "0"} and @{text "1"} for the
quotient type @{text int}.
*}
quotient_definition
"0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)" .
quotient_definition
"1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)" .
text {*
\noindent
To be useful, we can also need declare two operations for adding two
integers (written @{text plus}) and negating an integer
(written @{text "uminus"}).
*}
quotient_definition
"plus \<Colon> int \<Rightarrow> int \<Rightarrow> int" is add_pair
by auto
quotient_definition
"uminus \<Colon> int \<Rightarrow> int" is minus_pair
by auto
(*<*)
instance ..
end
(*>*)
text {*
\noindent
Isabelle/HOL can introduce some convenient short-hand notation for these
operations allowing the user to write
addition as infix operation, for example @{text "i + j"}, and
negation as prefix operation, for example @{text "- i"}. In both
cases, however, the declaration requires the user to discharge a
proof-obligation which ensures that the operations a
\emph{respectful}. This property ensures that the operations are
well-defined on the quotient level (a formal definition of
respectfulness will be given later). Both proofs can be solved by
the automatic proving tactic in Isabelle/HOL.
Besides helping with declarations of quotient types and definitions
of constants, the point of a quotient package is to help with
proving properties about quotient types. For example we might be
interested in the usual property that zero is an ???. This property
can be stated as follows:
*}
lemma zero_add:
shows "0 + i = (i::int)"
proof(descending)
txt {*
\noindent
The tactic @{text "descending"} automatically transfers this property of integers
to a proof-obligation involving pairs of @{typ nat}s. (There is also
a tactic, called @{text lifting}, which automatically transfers properties
from the raw level to the quotient type.) In case of lemma @{text "zero_add"}
we obtain the subgoal
\begin{isabelle}\ \ \ \ \ %%%
@{text "add_pair (0, 0) i \<approx> i"}
\end{isabelle}
\noindent
which can be solved again by the automatic proving tactic @{text "auto"}, as follows
*}
qed(auto)
text {*
In this simple example the task of the user is to state the property for integers
and use the quotient package and automatic proving tools of Isabelle/HOL to do
the ``rest''. A more interesting example is to establish an induction principle for
integers. For this we first establish the following induction principle where the
induction proceeds over two natural numbers.
*}
lemma nat_induct2:
assumes "P 0 0"
and "\<And>n m. P n m \<Longrightarrow> P (Suc n) m"
and "\<And>n m. P n m \<Longrightarrow> P n (Suc m)"
shows "P n m"
using assms
by (induction_schema) (pat_completeness, lexicographic_order)
text {*
\noindent
The symbol @{text "\<And>"} stands for Isabelle/HOL's universal quantifier and
@{text "\<Longrightarrow>"} for its implication.
As can be seen, this induction principle can be conveniently established using the
reasoning infrastructure of the function package \cite{???}, which
provides the tactics @{text "induction_schema"}, @{text "pat_completeness"}
and @{text "lexicographic_order"}. These tactics enable Isabelle/HOL
to use well-founded induction to prove @{text "nat_induct2"}. Our
quotient package can now be used to prove the following property:
*}
lemma int_induct:
assumes "P 0"
and "\<And>i. P i \<Longrightarrow> P (i + 1)"
and "\<And>i. P i \<Longrightarrow> P (i + (- 1))"
shows "P (j::int)"
using assms
proof (descending)
txt {*
\noindent
The @{text descending} tactic transfers it to the following proof
obligation on the raw level.
@{subgoals[display]}
\noindent
Note that the variable @{text "j"} in this subgoal is of type
@{text "nat \<times> nat"}. This subgoal cannot be proved automatically by
@{text auto}, but if we give it the hint to use @{text nat_induct2},
then @{text auto} can discharge it as follows.
*}
qed (auto intro: nat_induct2)
text {*
This completes the proof of the induction principle
for integers. Isabelle/HOL would allow us to inspect the
detailed reasoning steps involved which would confirm that
@{text "int_induct"} has been proved from ``first-principles''
by transforming the property over the quotient type @{text int}
to a corresponding property one on the raw level.
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:
%%% FIXME: Referee 1 says:
%%% Diagram is unclear. Firstly, isn't an existing type a "set (not sets) of raw elements"?
%%% Secondly, isn't the _set of_ equivalence classes mapped to and from the new type?
%%% Thirdly, what do the words "non-empty subset" refer to ?
%%% Cezary: I like the diagram, maybe 'new type' could be outside, but otherwise
%%% I wouldn't change it.
\begin{center}
\mbox{}\hspace{20mm}\begin{tikzpicture}[scale=1.1]
%%\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 is given by the user.
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 is
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
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@{thm concat.simps(1)[THEN eq_reflection]}\\
@{thm concat.simps(2)[THEN eq_reflection, where x1="x" and xs1="xs"]}
\end{tabular}
\end{isabelle}
\noindent
where @{text "@"} is the usual
list append. We expect that the corresponding
operator on finite sets, written @{term "fconcat"},
builds finite unions of finite sets:
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@{thm concat_empty_fset[THEN eq_reflection]}\\
@{thm concat_insert_fset[THEN eq_reflection, where x1="x" and S1="S"]}
\end{tabular}
\end{isabelle}
\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
\begin{isabelle}\ \ \ \ \ %%%
@{text "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}
\end{isabelle}
\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
\begin{isabelle}\ \ \ \ \ %%%
@{text "\<Union> S \<equiv> Abs_fset (flat ((map_list Rep_fset \<circ> Rep_fset) S))"}
\end{isabelle}
\noindent
where @{term map_list} 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}.
{\bf EXAMPLE BY HUFFMAN @{thm map_concat_fset}}
%%%TODO Update the contents.
In addition 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). A pleasing side-result
is that our procedure for lifting theorems is completely deterministic
following the structure of the theorem being lifted and the theorem
on the quotient level. {\it Space constraints, unfortunately, allow us to only
sketch this part of our work in Section 5 and we defer the reader to a longer
version for the details.} However, we will give in Section 3 and 4 all
definitions that specify the input and output data of our three-step
lifting procedure. Appendix A gives an example how our quotient
package works in practise.
*}
section {* Preliminaries and General Quotients\label{sec:prelims} *}
text {*
\noindent
We will give in this section a crude overview of HOL and describe the main
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
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
@{text "\<sigma>, \<tau> ::= \<alpha> | (\<sigma>,\<dots>, \<sigma>) \<kappa>"} &
@{text "t, s ::= x\<^isup>\<sigma> | c\<^isup>\<sigma> | t t | \<lambda>x\<^isup>\<sigma>. t"}\\
\end{tabular}
\end{isabelle}
\noindent
with types being either type variables or type constructors and terms
being variables, constants, applications or abstractions.
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; for example, a primitive constant is equality, with type @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
bool"}, and the identity function with type @{text "id :: \<sigma> \<Rightarrow> \<sigma>"} is
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 proof
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's, our work relies on map-functions defined for every type
constructor taking some arguments, for example @{text map_list} for lists. Homeier
describes in \cite{Homeier05} map-functions for products, sums, options and
also the following map for function types
\begin{isabelle}\ \ \ \ \ %%%
@{thm map_fun_def[THEN eq_reflection]}
\end{isabelle}
\noindent
Using this map-function, we can give the following, equivalent, but more
uniform definition for @{text add} shown in \eqref{adddef}:
\begin{isabelle}\ \ \ \ \ %%%
@{text "add \<equiv> (Rep_int \<singlearr> Rep_int \<singlearr> Abs_int) add_pair"}
\end{isabelle}
\noindent
Using extensionality and unfolding the definition of @{text "\<singlearr>"},
we can get back to \eqref{adddef}.
In what follows we shall use the convention to write @{text "map_\<kappa>"} for a map-function
of the type-constructor @{text \<kappa>}.
%% a general type for map all types is difficult to give (algebraic types are
%% easy, but for example the function type is not algebraic
%For a type @{text \<kappa>} with arguments @{text "\<alpha>\<^isub>1\<^isub>\<dots>\<^isub>n"} the
%type of the function @{text "map_\<kappa>"} has to be @{text "\<alpha>\<^isub>1\<Rightarrow>\<dots>\<Rightarrow>\<alpha>\<^isub>n\<Rightarrow>\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>n \<kappa>"}.
%For example @{text "map_list"}
%has to have the type @{text "\<alpha>\<Rightarrow>\<alpha> list"}.
In our implementation we maintain
a database of these 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
\begin{isabelle}\ \ \ \ \ %%%
@{text "(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"}
\end{isabelle}
\noindent
Homeier gives also the following operator for defining equivalence
relations over function types
%
\begin{isabelle}\ \ \ \ \ %%%
@{thm fun_rel_def[of "R\<^isub>1" "R\<^isub>2", THEN eq_reflection]}
\hfill\numbered{relfun}
\end{isabelle}
\noindent
In the context of quotients, the following two notions from \cite{Homeier05}
are needed later on.
\begin{definition}[Respects]\label{def:respects}
An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}.
\end{definition}
\begin{definition}[Bounded $\forall$ and $\lambda$]\label{def:babs}
@{text "\<forall>x \<in> S. P x"} holds if for all @{text x}, @{text "x \<in> S"} implies @{text "P x"};
and @{text "(\<lambda>x \<in> S. f x) x = f x"} provided @{text "x \<in> S"}.
\end{definition}
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"}
holds if and only if
\begin{isabelle}\ \ \ \ \ %%%%
\begin{tabular}{rl}
(i) & \begin{isa}@{thm (rhs1) Quotient_def[of "R"]}\end{isa}\\
(ii) & \begin{isa}@{thm (rhs2) Quotient_def[of "R"]}\end{isa}\\
(iii) & \begin{isa}@{thm (rhs3) Quotient_def[of "R"]}\end{isa}\\
\end{tabular}
\end{isabelle}
\end{definition}
\noindent
The value of this definition lies in the fact that validity of @{term "Quotient R Abs Rep"} can
often be proved in terms of the validity of @{term "Quot"} 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}
\begin{isa}
@{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{isa}
\end{proposition}
\noindent
As a result, Homeier is able to build an automatic prover that can nearly
always discharge a proof obligation involving @{text "Quot"}. Our quotient
package makes heavy
use of this part of Homeier's work including an extension
for dealing with \emph{conjugations} of equivalence relations\footnote{That are
symmetric by definition.} defined as follows:
%%% FIXME Referee 2 claims that composition-of-relations means OO, and this is also
%%% what wikipedia says. Any idea for a different name? Conjugation of Relations?
\begin{definition}%%[Composition of Relations]
@{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate
composition defined by
@{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
holds if and only if there exists a @{text y} such that @{thm (prem 1) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} and
@{thm (prem 2) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}.
\end{definition}
\noindent
Unfortunately a general quotient theorem for @{text "\<circ>\<circ>\<circ>"}, analogous to the one
for @{text "\<singlearr>"} given in Proposition \ref{funquot}, would not be true
in general. It cannot even be stated inside HOL, because of restrictions on types.
However, we can prove specific instances of a
quotient theorem for composing particular quotient relations.
For example, to lift theorems involving @{term flat} the quotient theorem for
composing @{text "\<approx>\<^bsub>list\<^esub>"} will be necessary: given @{term "Quotient R Abs Rep"}
with @{text R} being an equivalence relation, then
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{r@ {\hspace{1mm}}l}
@{text "Quot"} & @{text "(rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>)"}\\
& @{text "(Abs_fset \<circ> map_list Abs)"} @{text "(map_list Rep \<circ> Rep_fset)"}\\
\end{tabular}
\end{isabelle}
*}
section {* Quotient Types and Quotient Definitions\label{sec:type} *}
text {*
\noindent
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. The @{text "\<alpha>s"}
indicate the arity of the new type and the type-variables of @{text "\<sigma>"} can only
be contained in @{text "\<alpha>s"}. 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 are omitted). Given this data, we define for declarations shown in
\eqref{typedecl} the quotient types internally 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 constraint 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 then 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 holds for every quotient type
(for the proof see \cite{Homeier05}).
\begin{proposition}
\begin{isa}@{term "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.\end{isa}
\end{proposition}
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 (@{text "flat"} having the type
@{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"}).
From such declarations given by the user, the quotient package needs to derive proper
definitions using @{text "Abs"} and @{text "Rep"}. 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 shall give below. The idea behind
these two functions is to simultaneously 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. In what follows 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>n, \<tau>\<^isub>n)"}; similarly
for @{text REP}.
%
\begin{center}
\hfill
\begin{tabular}{@ {\hspace{2mm}}l@ {}}
\multicolumn{1}{@ {}l}{equal types:}\\
@{text "ABS (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\hspace{5mm}%\\
@{text "REP (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\
\multicolumn{1}{@ {}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{1}{@ {}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{1}{@ {}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
In the last two clauses are subtle. We rely in them on the fact 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"}). This data is given by declarations shown in \eqref{typedecl}.
The quotient construction ensures that the type variables in @{text
"\<rho>s \<kappa>"} must be among the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
substitutions for the @{text "\<alpha>s"} when matching @{text "\<sigma>s \<kappa>"} against
@{text "\<rho>s \<kappa>"}. This calculation determines what are the types in place
of the type variables @{text "\<alpha>s"} in the instance of
quotient type @{text "\<alpha>s \<kappa>\<^isub>q"}---namely @{text "\<tau>s"}, and the corresponding
types in place of the @{text "\<alpha>s"} in the raw type @{text "\<rho>s \<kappa>"}---namely @{text "\<sigma>s'"}. The
function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw
type as follows:
%
\begin{center}
\begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
@{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 in the first clause we can interpret type-variables @{text \<alpha>} as
term variables @{text a}. In the last clause we build an abstraction over all
term-variables of the map-function generated by the auxiliary function
@{text "MAP'"}.
The need for 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:
%%% FIXME: Reviewer 2 asks: last two lines defining ABS and REP for
%%% unequal type constructors: How are the $\varrho$s defined? The
%%% following paragraph mentions them, but this paragraph is unclear,
%%% since it then mentions $\alpha$s, which do not seem to be defined
%%% either. As a result, I do not understand the first two sentences
%%% in this paragraph. I can imagine roughly what the following
%%% sentence `The $\sigma$s' are given by the matchers for the
%%% $\alpha$s$ when matching $\varrho$s $\kappa$ against $\sigma$s
%%% $\kappa$.' means, but also think that it is too vague.
\begin{isabelle}\ \ \ \ \ %%%
@{text "\<lambda>a b. map_prod (map_list a) b"}
\end{isabelle}
\noindent
which is essential in order to define the corresponding 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 these types into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)
the abstraction function
\begin{isabelle}\ \ \ %%%
\begin{tabular}{l}
@{text "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr>"}\\
\mbox{}\hspace{4.5cm}@{text " Abs_fset \<circ> map_list id"}
\end{tabular}
\end{isabelle}
\noindent
In our implementation we further
simplify this function by rewriting with the usual laws about @{text
"map"}s and @{text "id"}, for example @{term "map_list id = id"} and @{text "f \<circ> id =
id \<circ> f = f"}. This gives us the simpler abstraction function
\begin{isabelle}\ \ \ \ \ %%%
@{text "(map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
\end{isabelle}
\noindent
which we can use for defining @{term "fconcat"} as follows
\begin{isabelle}\ \ \ \ \ %%%
@{text "\<Union> \<equiv> ((map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}
\end{isabelle}
\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
\begin{isabelle}\ \ \ \ \ %%%
\mbox{@{text "c \<equiv> ABS (\<sigma>, \<tau>) t"}}
\end{isabelle}
\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"} and @{text "REP"}.
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}
*}
section {* Respectfulness and Preservation \label{sec:resp} *}
text {*
\noindent
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 lifting process, we need to impose
two restrictions in form of proof obligations that arise during the
lifting. The reason is that even if definitions for all raw constants
can be given, \emph{not} all theorems can be lifted to the quotient type. Most
notable is the bound variable function, that is the constant @{text bn},
defined
for raw lambda-terms as follows
\begin{isabelle}
\begin{center}
@{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)"}\smallskip\\
@{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}
\end{center}
\end{isabelle}
\noindent
We can generate a definition for this constant using @{text ABS} and @{text REP}.
But this constant does \emph{not} respect @{text "\<alpha>"}-equivalence and
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{respectfulness} and \emph{preservation}. We have
to slightly extend Homeier's definitions in order to deal with quotient
compositions.
%%% FIXME: Reviewer 3 asks why are the definitions that follow enough to deal
%%% with quotient composition.
To formally define what respectfulness is, we have to first define
the notion of \emph{aggregate equivalence relations} using the function @{text "REL(\<sigma>, \<tau>)"}
The idea behind this function is to simultaneously descend into the raw types
@{text \<sigma>} and quotient types @{text \<tau>}, and generate the appropriate
quotient equivalence relations in places where the types differ and equalities
elsewhere.
\begin{center}
\hfill
\begin{tabular}{l}
\multicolumn{1}{@ {}l}{equal types:}
@{text "REL (\<sigma>, \<sigma>)"} $\dn$ @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
\multicolumn{1}{@ {}l}{equal type constructors:}\\
@{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
\multicolumn{1}{@ {}l}{unequal type constructors:}\\
@{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} $\dn$ @{text "rel_\<kappa>\<^isub>q (REL (\<sigma>s', \<tau>s))"}\\
\end{tabular}\hfill\numbered{REL}
\end{center}
\noindent
The @{text "\<sigma>s'"} in the last clause are calculated as in \eqref{ABSREP}:
again we know that type @{text "\<alpha>s \<kappa>\<^isub>q"} is the quotient of the raw type
@{text "\<rho>s \<kappa>"}. The @{text "\<sigma>s'"} are the substitutions for @{text "\<alpha>s"} obtained by matching
@{text "\<rho>s \<kappa>"} and @{text "\<sigma>s \<kappa>"}.
Let us return to the lifting procedure of theorems. Assume we have a theorem
that contains the raw constant @{text "c\<^isub>r :: \<sigma>"} and which we want to
lift to a theorem where @{text "c\<^isub>r"} is replaced by the corresponding
constant @{text "c\<^isub>q :: \<tau>"} defined over a quotient type. In this situation
we generate the following proof obligation
\begin{isabelle}\ \ \ \ \ %%%
@{text "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}.
\end{isabelle}
\noindent
Homeier calls these proof obligations \emph{respectfulness
theorems}. However, unlike his quotient package, we might have several
respectfulness theorems for one constant---he has at most one.
The reason is that because of our quotient compositions, the types
@{text \<sigma>} and @{text \<tau>} are not completely determined by @{text "c\<^bsub>r\<^esub>"}.
And for every instantiation of the types, a corresponding
respectfulness theorem is necessary.
Before lifting a theorem, we require the user to discharge
respectfulness proof obligations. In case of @{text bn}
this obligation is %%as follows
\begin{isabelle}\ \ \ \ \ %%%
@{text "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
\end{isabelle}
\noindent
and the point is that the user cannot discharge it: because it is not true. To see this,
we can just unfold the definition of @{text "\<doublearr>"} \eqref{relfun}
using extensionality to obtain the false statement
\begin{isabelle}\ \ \ \ \ %%%
@{text "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 then bn(t\<^isub>1) = bn(t\<^isub>2)"}
\end{isabelle}
\noindent
In contrast, lifting a theorem about @{text "append"} to a theorem describing
the union of finite sets will mean to discharge the proof obligation
\begin{isabelle}\ \ \ \ \ %%%
@{text "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}
\end{isabelle}
\noindent
To do so, we have to establish
\begin{isabelle}\ \ \ \ \ %%%
if @{text "xs \<approx>\<^bsub>list\<^esub> ys"} and @{text "us \<approx>\<^bsub>list\<^esub> vs"}
then @{text "xs @ us \<approx>\<^bsub>list\<^esub> ys @ vs"}
\end{isabelle}
\noindent
which is straightforward given the definition shown in \eqref{listequiv}.
The second restriction we have to impose arises from non-lifted polymorphic
constants, which are instantiated to a type being quotient. For example,
take the @{term "cons"}-constructor to add a pair of natural numbers to a
list, whereby we assume the pair of natural numbers turns into an integer in
the quotient construction. The point is that we still want to use @{text
cons} for adding integers to lists---just with a different type. To be able
to lift such theorems, we need a \emph{preservation property} for @{text
cons}. Assuming we have a polymorphic raw constant @{text "c\<^isub>r :: \<sigma>"}
and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"}, then a
preservation property is as follows
%%% FIXME: Reviewer 2 asks: You say what a preservation theorem is,
%%% but not which preservation theorems you assume. Do you generate a
%%% proof obligation for a preservation theorem for each raw constant
%%% and its corresponding lifted constant?
%%% Cezary: I think this would be a nice thing to do but we have not
%%% done it, the theorems need to be 'guessed' from the remaining obligations
\begin{isabelle}\ \ \ \ \ %%%
@{text "Quot R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"}
\end{isabelle}
\noindent
where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}.
In case of @{text cons} (which has type @{text "\<alpha> \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"}) we have
\begin{isabelle}\ \ \ \ \ %%%
@{text "(Rep \<singlearr> map_list Rep \<singlearr> map_list Abs) cons = cons"}
\end{isabelle}
\noindent
under the assumption @{term "Quotient R Abs Rep"}. The point is that if we have
an instance of @{text cons} where the type variable @{text \<alpha>} is instantiated
with @{text "nat \<times> nat"} and we also quotient this type to yield integers,
then we need to show this preservation property.
%%%@ {thm [display, indent=10] Cons_prs2}
%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_list Abs) (map_list 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 {*
%%% FIXME Reviewer 3 asks: Section 5 shows the technicalities of
%%% lifting theorems. But there is no clarification about the
%%% correctness. A reader would also be interested in seeing some
%%% discussions about the generality and limitation of the approach
%%% proposed there
%%% TODO: This introduction is same as the introduction to the previous section.
\noindent
The main benefit of a quotient package is to lift automatically theorems over raw
types to theorems over quotient types. We will perform this lifting in
three phases, called \emph{regularization},
\emph{injection} and \emph{cleaning} according to procedures in Homeier's ML-code.
Space restrictions, unfortunately, prevent us from giving anything but a sketch of these three
phases. However, we will precisely define the input and output data of these phases
(this was omitted in \cite{Homeier05}).
The purpose of regularization is to change the quantifiers and abstractions
in a ``raw'' theorem to quantifiers over variables that respect their respective relations
(Definition \ref{def:respects} states what respects means). The purpose of injection is to add @{term Rep}
and @{term Abs} of appropriate types in front of constants and variables
of the raw type so that they can be replaced by the corresponding constants from the
quotient type. The purpose of cleaning is to bring the theorem derived in the
first two phases into the form the user has specified. Abstractly, our
package establishes the following three proof steps:
%%% FIXME: Reviewer 1 complains that the reader needs to guess the
%%% meaning of reg_thm and inj_thm, as well as the arguments of REG
%%% which are given above. I wouldn't change it.
\begin{center}
\begin{tabular}{l@ {\hspace{4mm}}l}
1.) Regularization & @{text "raw_thm \<longrightarrow> reg_thm"}\\
2.) Injection & @{text "reg_thm \<longleftrightarrow> inj_thm"}\\
3.) Cleaning & @{text "inj_thm \<longleftrightarrow> quot_thm"}\\
\end{tabular}
\end{center}
\noindent
which means, stringed together, the raw theorem implies the quotient theorem.
The core of the quotient package requires both the @{text "raw_thm"} (as a
theorem) and the \emph{term} of the @{text "quot_thm"}. This lets the user
have a finer control over which parts of a raw theorem should be lifted.
We also provide more automated modes where either the @{text "quot_thm"}
is guessed from the form of @{text "raw_thm"} or the @{text "raw_thm"} is
guessed from the current goal and these are described in Section \ref{sec:descending}.
The second and third proof step performed in package will always succeed if the appropriate
respectfulness and preservation theorems are given. In contrast, the first
proof step can fail: a theorem given by the user does not always
imply a regularized version and a stronger one needs to be proved. An example
for this kind of failure is the simple statement for integers @{text "0 \<noteq> 1"}.
One might hope that it can be proved by lifting @{text "(0, 0) \<noteq> (1, 0)"},
but this raw theorem only shows that two particular elements in the
equivalence classes are not equal. In order to obtain @{text "0 \<noteq> 1"}, a
more general statement stipulating that the equivalence classes are not
equal is necessary. This kind of failure is beyond the scope where the
quotient package can help: the user has to provide a raw theorem that
can be regularized automatically, or has to provide an explicit proof
for the first proof step. Homeier gives more details about this issue
in the long version of \cite{Homeier05}.
In the following we will first define the statement of the
regularized theorem based on @{text "raw_thm"} and
@{text "quot_thm"}. Then we define the statement of the injected theorem, based
on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps,
which can all be performed independently from each other.
We first define the function @{text REG}, which takes the terms of the
@{text "raw_thm"} and @{text "quot_thm"} as input and returns
@{text "reg_thm"}. The idea
behind this function is that it replaces quantifiers and
abstractions involving raw types by bounded ones, and equalities
involving raw types by appropriate aggregate
equivalence relations. It is defined by simultaneous recursion on
the structure of the terms of @{text "raw_thm"} and @{text "quot_thm"} as follows:
%
\begin{center}
\begin{tabular}{@ {}l@ {}}
\multicolumn{1}{@ {}l@ {}}{abstractions:}\\%%\smallskip\\
@{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} $\dn$
$\begin{cases}
@{text "\<lambda>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
@{text "\<lambda>x\<^sup>\<sigma> \<in> Resp (REL (\<sigma>, \<tau>)). REG (t, s)"}
\end{cases}$\\%%\smallskip\\
\multicolumn{1}{@ {}l@ {}}{universal quantifiers:}\\
@{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} $\dn$
$\begin{cases}
@{text "\<forall>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
@{text "\<forall>x\<^sup>\<sigma> \<in> Resp (REL (\<sigma>, \<tau>)). REG (t, s)"}
\end{cases}$\\%%\smallskip\\
\multicolumn{1}{@ {}l@ {}}{equality: \hspace{3mm}%%}\smallskip\\
%% REL of two equal types is the equality so we do not need a separate case
@{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} $\dn$ @{text "REL (\<sigma>, \<tau>)"}}\smallskip\\
\multicolumn{1}{@ {}l@ {}}{applications, variables and 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 (x\<^isub>1, x\<^isub>2)"} $\dn$ @{text "x\<^isub>1"}\\
@{text "REG (c\<^isub>1, c\<^isub>2)"} $\dn$ @{text "c\<^isub>1"}\\
\end{tabular}
\end{center}
%
\noindent
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 as argument
@{text "reg_thm"} and @{text "quot_thm"} (both as
terms) and returns @{text "inj_thm"}:
\begin{center}
\begin{tabular}{l}
\multicolumn{1}{@ {}l}{abstractions:}\\
@{text "INJ (\<lambda>x. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} $\dn$\\
\hspace{18mm}$\begin{cases}
@{text "\<lambda>x. INJ (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
@{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x. INJ (t, s)))"}
\end{cases}$\smallskip\\
@{text "INJ (\<lambda>x \<in> R. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} $\dn$\\
\hspace{18mm}@{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x \<in> R. INJ (t, s)))"}\smallskip\\
\multicolumn{1}{@ {}l}{universal quantifiers:}\\
@{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"}\smallskip\\
\multicolumn{1}{@ {}l}{applications, variables and constants:}\smallskip\\
@{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 (x\<^isub>1\<^sup>\<sigma>, x\<^isub>2\<^sup>\<tau>) "} $\dn$
$\begin{cases}
@{text "x\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
@{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) x\<^isub>1)"}\\
\end{cases}$\\
@{text "INJ (c\<^isub>1\<^sup>\<sigma>, c\<^isub>2\<^sup>\<tau>) "} $\dn$
$\begin{cases}
@{text "c\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
@{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) c\<^isub>1)"}\\
\end{cases}$\\
\end{tabular}
\end{center}
\noindent
In this definition we again omitted the cases for existential and unique existential
quantifiers.
%%% FIXME: Reviewer2 citing following sentence: You mention earlier
%%% that this implication may fail to be true. Does that meant that
%%% the `first proof step' is a heuristic that proves the implication
%%% raw_thm \implies reg_thm in some instances, but fails in others?
%%% You should clarify under which circumstances the implication is
%%% being proved here.
%%% Cezary: It would be nice to cite Homeiers discussions in the
%%% Quotient Package manual from HOL (the longer paper), do you agree?
In the first phase, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always
start with an implication. Isabelle provides \emph{mono} rules that can split up
the implications into simpler implicational subgoals. This succeeds for every
monotone connective, except in places where the function @{text REG} replaced,
for instance, a quantifier by a bounded quantifier. To decompose them, we have
to prove that the relations involved are aggregate equivalence relations.
%In this case we have
%rules of the form
%
% \begin{isabelle}\ \ \ \ \ %%%
%@{text "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}
%\end{isabelle}
%\noindent
%They decompose a bounded quantifier on the right-hand side. We can decompose a
%bounded quantifier anywhere if R is an equivalence relation or
%if it is a relation over function types with the range being an equivalence
%relation. If @{text R} is an equivalence relation we can prove that
%\begin{isabelle}\ \ \ \ \ %%%
%@{text "\<forall>x \<in> Resp R. P x = \<forall>x. P x"}
%\end{isabelle}
%\noindent
%If @{term R\<^isub>2} is an equivalence relation, we can prove that for any predicate @{term P}
%%% FIXME Reviewer 1 claims the theorem is obviously false so maybe we
%%% should include a proof sketch?
%\begin{isabelle}\ \ \ \ \ %%%
%@{thm (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2]}
%\end{isabelle}
%\noindent
%The last theorem is new in comparison with Homeier's package. There the
%injection procedure would be used to prove such goals and
%the assumption about the equivalence relation would be used. We use the above theorem directly,
%because this allows us to completely separate the first and the second
%proof step into two independent ``units''.
The second phase, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"}, starts with an equality
between the terms of the regularized theorem and the injected theorem.
The proof again follows the structure of the
two underlying terms taking respectfulness theorems into account.
%\begin{itemize}
%\item For two constants an appropriate respectfulness theorem is applied.
%\item For two variables, we use the assumptions proved in the regularization step.
%\item For two abstractions, we @{text "\<eta>"}-expand and @{text "\<beta>"}-reduce them.
%\item For two applications, we check that the right-hand side is an application of
% @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"} holds. If yes then we
% can apply the theorem:
%\begin{isabelle}\ \ \ \ \ %%%
% @{term "R x y \<longrightarrow> R x (Rep (Abs y))"}
%\end{isabelle}
% Otherwise we introduce an appropriate relation between the subterms
% and continue with two subgoals using the lemma:
%\begin{isabelle}\ \ \ \ \ %%%
% @{text "(R\<^isub>1 \<doublearr> R\<^isub>2) f g \<longrightarrow> R\<^isub>1 x y \<longrightarrow> R\<^isub>2 (f x) (g y)"}
%\end{isabelle}
%\end{itemize}
We defined the theorem @{text "inj_thm"} in such a way that
establishing in the third phase the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be
achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient
definitions. This step also requires that the definitions of all lifted constants
are used to fold the @{term Rep} with the raw constants. We will give more details
about our lifting procedure in a longer version of this paper.
%Next for
%all abstractions and quantifiers the lambda and
%quantifier preservation theorems are used to replace the
%variables that include raw types with respects by quantifiers
%over variables that include quotient types. We show here only
%the lambda preservation theorem. Given
%@{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}, we have:
%\begin{isabelle}\ \ \ \ \ %%%
%@{thm (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2"]}
%\end{isabelle}
%\noindent
%Next, relations over lifted types can be rewritten to equalities
%over lifted type. Rewriting is performed with the following theorem,
%which has been shown by Homeier~\cite{Homeier05}:
%\begin{isabelle}\ \ \ \ \ %%%
%@{thm (concl) Quotient_rel_rep}
%\end{isabelle}
%Finally, we rewrite with the preservation theorems. This will result
%in two equal terms that can be solved by reflexivity.
*}
section {* Derivation of the shape of lifted and raw theorems\label{sec:descending} *}
text {*
In the previous sections we have assumed, that the user specifies
both the raw theorem and the statement of the quotient one.
This allows complete flexibility, as to which parts of the statement
are lifted to the quotient level and which are intact. In
other implementations of automatic quotients (for example Homeier's
package) only the raw theorem is given to the quotient package and
the package is able to guess the quotient one. In this
section we give examples where there are multiple possible valid lifted
theorems starting from a raw one. We also show a heuristic for
computing the quotient theorem from a raw one, and a mechanism for
guessing a raw theorem starting with a quotient one.
*}
subsection {* Multiple lifted theorems *}
text {*
There are multiple reasons why multiple valid lifted theorems can arize.
Below we describe three possible scenarios: multiple raw variable,
multiple quotients for the same raw type and multiple quotients.
Given a raw theorem there are often several variables that include
a raw type. It this case, one can choose which of the variables to
lift. In certain cases this can lead to a number of valid theorem
statements, however type constraints may disallow certain combinations.
Lets see an example where multiple variables can have different types.
The Isabelle/HOL induction principle for two lists is:
\begin{isabelle}\ \ \ \ \ %%%
@{thm list_induct2'}
\end{isabelle}
the conclusion is a predicate of the form @{text "P xs ys"}, where
the two variables are lists. When lifting such theorem to the quotient
type one can choose if one want to quotient @{text "xs"} or @{text "ys"}, or
both. All these give rise to valid quotiented theorems, however the
automatic mode (or other quotient packages) would derive only the version
with both being quotiented, namely:
\begin{isabelle}\ \ \ \ \ %%%
@{thm list_induct2'[quot_lifted]}
\end{isabelle}
A second scenario, where multiple possible quotient theorems arise is
when a single raw type is used in two quotients. Consider three quotients
of the list type: finite sets, finite multisets and lists with distinct
elements. We have developed all three types with the help of the quotient
package. Given a theorem that talks about lists --- for example the regular
induction principle --- one can lift it to three possible theorems: the
induction principle for finite sets, induction principle for finite
multisets or the induction principle for distinct lists. Again given an
induction principle for two lists this gives rise to 15 possible valid
lifted theorems.
In our developments using the quotient package we also encountered a
scenario where multiple valid theorem statements arise, but the raw
types are not identical. Consider the type of lambda terms, where the
variables are indexed with strings. Quotienting lambda terms by alpha
equivalence gives rise to a Nominal construction~\cite{Nominal}. However
at the same time the type of strings being a list of characters can
lift to theorems about finite sets of characters.
*}
subsection {* Derivation of the shape of theorems *}
text {*
To derive a the shape of a lifted or raw theorem the quotient package
first builds a type and term substitution.
The list of type substitution is created by taking the pairs
@{text "(raw_type, quotient_type)"} for every user defined quotient.
The term substitutions are of two types: First for every user-defined
quotient constant, the pair @{text "(raw_term, quotient_constant)"}
is included in the substitution. Second, for every quotient relation
@{text "\<approx>"} the pair @{text "(\<approx>, =)"} with the equality being the
equality on the defined quotient type is included in the substitution.
The derivation function next traverses the theorem statement expressed
as a term and replaces the types of all free variables and of all
lambda-abstractions using the type substitution. For every constant
is not matched by the term substitution and we perform the type substitution
on the type of the constant (this is necessary for quotienting theorems
with polymorphic constants) or the type of the substitution is matched
and the match is returned.
The heuristic defined above is greedy and according to our experience
this is what the user wants. The procedure may in some cases produce
theorem statements that do not type-check. However verifying all
possible theorem statements is too costly in general.
*}
subsection {* Interaction modes and derivation of the the shape of theorems *}
text {*
In the quotient package we provide three interaction modes, that use
can the procedure procedure defined in the previous subsection.
First, the completely manual mode which we implemented as the
Isabelle method @{text lifting}. In this mode the user first
proves the raw theorem. Then the lifted theorem can be proved
by the method lifting, that takes the reference to the raw theorem
(or theorem list) as an argument. Such completely manual mode is
necessary for theorems where the specification of the lifted theorem
from the raw one is not unique, which we discussed in the previous
subsection.
Next, we provide a mode for automatically lifting a given
raw theorem. We implemented this mode as an isabelle attribute,
so given the raw theorem @{text thm}, the user can refer to the
theorem @{text "thm[quot_lifted]"}.
Finally we provie a method for translating a given quotient
level theorem to a raw one. We implemented this as an Isabelle
method @{text descending}. The user starts with expressing a
quotient level theorem statement and applies this method.
The quotient package derives a raw level statement and assumes
it as a subgoal. Given that this subgoal is proved, the quotient
package can lift the raw theorem fulfilling the proof of the
original lifted theorem statement.
*}
section {* Conclusion and Related Work\label{sec:conc}*}
text {*
\noindent
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/}.}
The package is
heavily used in the new version of Nominal Isabelle, which provides a
convenient reasoning infrastructure for programming language calculi
involving general binders. To achieve this, it builds types representing
@{text \<alpha>}-equivalent terms. 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}.
{\bf INSTEAD OF NOMINAL WORK, GIVE WORK BY BULWAHN ET AL?}
There is a wide range of existing literature for dealing with quotients
in theorem provers. Slotosch~\cite{Slotosch97} implemented a mechanism that
automatically defines quotient types for Isabelle/HOL. But he did not
include theorem lifting. Harrison's quotient package~\cite{harrison-thesis}
is the first one that is able to automatically lift theorems, however only
first-order theorems (that is theorems where abstractions, quantifiers and
variables do not involve functions that include the quotient type). There is
also some work on quotient types in non-HOL based systems and logical
frameworks, including theory interpretations in
PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, and
setoids in Coq \cite{ChicliPS02}. Paulson showed a construction of
quotients that does not require the Hilbert Choice operator, but also only
first-order theorems can be lifted~\cite{Paulson06}. The most related work
to our package is the package for HOL4 by Homeier~\cite{Homeier05}. He
introduced most of the abstract notions about quotients and also deals with
lifting of higher-order theorems. However, he cannot deal with quotient
compositions (needed for lifting theorems about @{text flat}). Also, a
number of his definitions, like @{text ABS}, @{text REP} and @{text INJ} etc
only exist in \cite{Homeier05} as ML-code, not included in the paper.
Like Homeier's, our quotient package can deal with partial equivalence
relations, but for lack of space we do not describe the mechanisms
needed for this kind of quotient constructions.
%%% FIXME Reviewer 3 would like to know more about the lifting in Coq and PVS,
%%% and some comparison. I don't think we have the space for any additions...
One feature of our quotient package is that when lifting theorems, the user
can precisely specify what the lifted theorem should look like. This feature
is necessary, for example, when lifting an induction principle for two
lists. Assuming this principle has as the conclusion a predicate of the
form @{text "P xs ys"}, then we can precisely specify whether we want to
quotient @{text "xs"} or @{text "ys"}, or both. We found this feature very
useful in the new version of Nominal Isabelle, where such a choice is
required to generate a reasoning infrastructure for alpha-equated terms.
%%
%% give an example for this
%%
\smallskip
\noindent
{\bf Acknowledgements:} We would like to thank Peter Homeier for the many
discussions about his HOL4 quotient package and explaining to us
some of its finer points in the implementation. Without his patient
help, this work would have been impossible. We would like to thank
Andreas Lochbiler for his comments on the first version of the quotient
package, in particular for the suggestions about the descending method.
*}
text_raw {*
%%\bibliographystyle{abbrv}
\bibliography{root}
\appendix
*}
section {* Examples \label{sec:examples} *}
text {*
%%% FIXME Reviewer 1 would like an example of regularized and injected
%%% statements. He asks for the examples twice, but I would still ignore
%%% it due to lack of space...
\noindent
In this appendix we will show a sequence of declarations for defining the
type of integers by quotienting pairs of natural numbers, and
lifting one theorem.
A user of our quotient package first needs to define a relation on
the raw type with which the quotienting will be performed. We give
the same integer relation as the one presented in \eqref{natpairequiv}:
\begin{isabelle}\ \ \ \ \ %
\begin{tabular}{@ {}l}
\isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"}\\
\isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"}
\end{tabular}
\end{isabelle}
\noindent
Next the quotient type must be defined. This generates a proof obligation that the
relation is an equivalence relation, which is solved automatically using the
definition of equivalence and extensionality:
\begin{isabelle}\ \ \ \ \ %
\begin{tabular}{@ {}l}
\isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"}\\
\hspace{5mm}@{text "by (auto simp add: equivp_def expand_fun_eq)"}
\end{tabular}
\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)"}\\[3mm]
\isacommand{fun}~~@{text "add_pair"}\\
\isacommand{where}~~%
@{text "add_pair (m, n) (p, q) \<equiv> (m + p :: nat, n + q :: nat)"}\\
\isacommand{quotient\_definition}~~@{text "+ :: int \<Rightarrow> int \<Rightarrow> int"}~~%
\isacommand{is}~~@{text "add_pair"}\\
\end{tabular}
\end{isabelle}
\noindent
The following theorem about addition on the raw level can be proved.
\begin{isabelle}\ \ \ \ \ %
\isacommand{lemma}~~@{text "add_pair_zero: int_rel (add_pair (0, 0) x) x"}
\end{isabelle}
\noindent
If the user lifts this theorem, the quotient package performs all the lifting
automatically leaving the respectfulness proof for the constant @{text "add_pair"}
as the only remaining proof obligation. This property needs to be proved by the user:
\begin{isabelle}\ \ \ \ \ %
\begin{tabular}{@ {}l}
\isacommand{lemma}~~@{text "[quot_respect]:"}\\
@{text "(int_rel \<doublearr> int_rel \<doublearr> int_rel) add_pair add_pair"}
\end{tabular}
\end{isabelle}
\noindent
It can be discharged automatically by Isabelle when hinting to unfold the definition
of @{text "\<doublearr>"}.
After this, the user can prove the lifted lemma as follows:
\begin{isabelle}\ \ \ \ \ %
\isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting add_pair_zero"}
\end{isabelle}
\noindent
or by using the completely automated mode stating just:
\begin{isabelle}\ \ \ \ \ %
\isacommand{thm}~~@{text "add_pair_zero[quot_lifted]"}
\end{isabelle}
\noindent
Both methods give the same result, namely @{text "0 + x = x"}
where @{text x} is of type integer.
Although seemingly simple, arriving at this result without the help of a quotient
package requires a substantial reasoning effort (see \cite{Paulson06}).
{\bf \begin{itemize}
\item explain how Quotient R Abs Rep is proved
\item Type maps and Relation maps (show the case for functions)
\item Quotient extensions (quot\_thms)
\item Respectfulness and preservation
- Show special cases for quantifiers and lambda
- How do prs theorems look like for quotient compositions
\item Quotient-type locale
- Show the proof as much simpler than Homeier's one
\item ??? Infrastructure for storing theorems (rsp, prs, eqv, quot and idsimp)
\item Lifting vs Descending vs quot\_lifted
- automatic theorem translation heuristic
\item Partial equivalence quotients
- Bounded abstraction
- Respects
- partial descending
\item The heuristics for automatic regularization, injection and cleaning.
\item A complete example of a lifted theorem together with the regularized
injected and cleaned statement
\item Examples of quotients and properties that we used the package for.
\item co/contra-variance from Ondrej should be taken into account
\item give an example where precise specification of goal is necessary
\item mention multiple map\_prs2 theorems for compositional quotients
\end{itemize}}
*}
(*<*)
end
(*>*)