--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quotient-Paper/Paper-old.thy Fri Aug 27 13:57:00 2010 +0800
@@ -0,0 +1,1239 @@
+(*<*)
+theory Paper
+imports "Quotient"
+ "LaTeXsugar"
+ "../Nominal/FSet"
+begin
+
+(****
+
+** things to do for the next version
+*
+* - what are quot_thms?
+* - what do all preservation theorems look like,
+ in particular preservation for quotient
+ compositions
+ - explain how Quotient R Abs Rep is proved (j-version)
+ - give an example where precise specification helps (core Haskell in nominal?)
+
+ - Quote from Peter:
+
+ One might think quotient have been studied to death, but
+
+ - Mention Andreas Lochbiler in Acknowledgements and 'desceding'.
+
+*)
+
+notation (latex output)
+ rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
+ pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
+ "op -->" (infix "\<longrightarrow>" 100) and
+ "==>" (infix "\<Longrightarrow>" 100) and
+ fun_map ("_ \<^raw:\mbox{\singlearr}> _" 51) and
+ fun_rel ("_ \<^raw:\mbox{\doublearr}> _" 51) and
+ list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
+ fempty ("\<emptyset>") and
+ funion ("_ \<union> _") and
+ finsert ("{_} \<union> _") and
+ Cons ("_::_") and
+ concat ("flat") and
+ fconcat ("\<Union>")
+
+
+
+ML {*
+fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;
+
+fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
+ let
+ val concl =
+ Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)
+ in
+ case concl of (_ $ l $ r) => proj (l, r)
+ | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
+ end);
+*}
+
+setup {*
+ Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #>
+ Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #>
+ Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))
+*}
+
+(*>*)
+
+
+section {* Introduction *}
+
+text {*
+ \begin{flushright}
+ {\em ``Not using a [quotient] package has its advantages: we do not have to\\
+ collect all the theorems we shall ever want into one giant list;''}\\
+ Larry Paulson \cite{Paulson06}
+ \end{flushright}
+
+ \noindent
+ Isabelle is a popular generic theorem prover in which many logics can be
+ implemented. The most widely used one, however, is Higher-Order Logic
+ (HOL). This logic consists of a small number of axioms and inference rules
+ over a simply-typed term-language. Safe reasoning in HOL is ensured by two
+ very restricted mechanisms for extending the logic: one is the definition of
+ new constants in terms of existing ones; the other is the introduction of
+ new types by identifying non-empty subsets in existing types. It is well
+ understood how to use both mechanisms for dealing with quotient
+ constructions in HOL (see \cite{Homeier05,Paulson06}). For example the
+ integers in Isabelle/HOL are constructed by a quotient construction over the
+ type @{typ "nat \<times> nat"} and the equivalence relation
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + m\<^isub>2 = m\<^isub>1 + n\<^isub>2"}\hfill\numbered{natpairequiv}
+ \end{isabelle}
+
+ \noindent
+ This constructions yields the new type @{typ int} and definitions for @{text
+ "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of
+ natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations
+ such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in
+ terms of operations on pairs of natural numbers (namely @{text
+ "add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2,
+ m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}).
+ Similarly one can construct the type of finite sets, written @{term "\<alpha> fset"},
+ by quotienting the type @{text "\<alpha> list"} according to the equivalence relation
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}\hfill\numbered{listequiv}
+ \end{isabelle}
+
+ \noindent
+ which states that two lists are equivalent if every element in one list is
+ also member in the other. The empty finite set, written @{term "{||}"}, can
+ then be defined as the empty list and the union of two finite sets, written
+ @{text "\<union>"}, as list append.
+
+ Quotients are important in a variety of areas, but they are really ubiquitous in
+ the area of reasoning about programming language calculi. A simple example
+ is the lambda-calculus, whose raw terms are defined as
+
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "t ::= x | t t | \<lambda>x.t"}\hfill\numbered{lambda}
+ \end{isabelle}
+
+ \noindent
+ The problem with this definition arises, for instance, when one attempts to
+ prove formally the substitution lemma \cite{Barendregt81} by induction
+ over the structure of terms. This can be fiendishly complicated (see
+ \cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof
+ about raw lambda-terms). In contrast, if we reason about
+ $\alpha$-equated lambda-terms, that means terms quotient according to
+ $\alpha$-equivalence, then the reasoning infrastructure provided,
+ for example, by Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal
+ proof of the substitution lemma almost trivial.
+
+ The difficulty is that in order to be able to reason about integers, finite
+ sets or $\alpha$-equated lambda-terms one needs to establish a reasoning
+ infrastructure by transferring, or \emph{lifting}, definitions and theorems
+ from the raw type @{typ "nat \<times> nat"} to the quotient type @{typ int}
+ (similarly for finite sets and $\alpha$-equated lambda-terms). This lifting
+ usually requires a \emph{lot} of tedious reasoning effort \cite{Paulson06}.
+ It is feasible to do this work manually, if one has only a few quotient
+ constructions at hand. But if they have to be done over and over again, as in
+ Nominal Isabelle, then manual reasoning is not an option.
+
+ The purpose of a \emph{quotient package} is to ease the lifting of theorems
+ and automate the reasoning as much as possible. In the
+ context of HOL, there have been a few quotient packages already
+ \cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier
+ \cite{Homeier05} implemented in HOL4. The fundamental construction these
+ quotient packages perform can be illustrated by the following picture:
+
+%%% 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}
+ %%\draw[step=2mm] (-4,-1) grid (4,1);
+
+ \draw[very thick] (0.7,0.3) circle (4.85mm);
+ \draw[rounded corners=1mm, very thick] ( 0.0,-0.9) rectangle ( 1.8, 0.9);
+ \draw[rounded corners=1mm, very thick] (-1.95,0.8) rectangle (-2.9,-0.195);
+
+ \draw (-2.0, 0.8) -- (0.7,0.8);
+ \draw (-2.0,-0.195) -- (0.7,-0.195);
+
+ \draw ( 0.7, 0.23) node {\begin{tabular}{@ {}c@ {}}equiv-\\[-1mm]clas.\end{tabular}};
+ \draw (-2.45, 0.35) node {\begin{tabular}{@ {}c@ {}}new\\[-1mm]type\end{tabular}};
+ \draw (1.8, 0.35) node[right=-0.1mm]
+ {\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw elements)\end{tabular}};
+ \draw (0.9, -0.55) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
+
+ \draw[->, very thick] (-1.8, 0.36) -- (-0.1,0.36);
+ \draw[<-, very thick] (-1.8, 0.16) -- (-0.1,0.16);
+ \draw (-0.95, 0.26) node[above=0.4mm] {@{text Rep}};
+ \draw (-0.95, 0.26) node[below=0.4mm] {@{text Abs}};
+
+ \end{tikzpicture}
+ \end{center}
+
+ \noindent
+ The starting point is an existing type, to which we refer as the
+ \emph{raw type} and over which an equivalence relation given by the user is
+ defined. With this input the package introduces a new type, to which we
+ refer as the \emph{quotient type}. This type comes with an
+ \emph{abstraction} and a \emph{representation} function, written @{text Abs}
+ and @{text Rep}.\footnote{Actually slightly more basic functions are given;
+ the functions @{text Abs} and @{text Rep} need to be derived from them. We
+ will show the details later. } They relate elements in the
+ existing type to elements in the new type and vice versa, and can be uniquely
+ identified by their quotient type. For example for the integer quotient construction
+ the types of @{text Abs} and @{text Rep} are
+
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "Abs :: nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep :: int \<Rightarrow> nat \<times> nat"}
+ \end{isabelle}
+
+ \noindent
+ We therefore often write @{text Abs_int} and @{text Rep_int} if the
+ typing information is important.
+
+ Every abstraction and representation function stands for an isomorphism
+ between the non-empty subset and elements in the new type. They are
+ necessary for making definitions involving the new type. For example @{text
+ "0"} and @{text "1"} of type @{typ int} can be defined as
+
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "0 \<equiv> Abs_int (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs_int (1, 0)"}
+ \end{isabelle}
+
+ \noindent
+ Slightly more complicated is the definition of @{text "add"} having type
+ @{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition is as follows
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "add n m \<equiv> Abs_int (add_pair (Rep_int n) (Rep_int m))"}
+ \hfill\numbered{adddef}
+ \end{isabelle}
+
+ \noindent
+ where we take the representation of the arguments @{text n} and @{text m},
+ add them according to the function @{text "add_pair"} and then take the
+ abstraction of the result. This is all straightforward and the existing
+ quotient packages can deal with such definitions. But what is surprising 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
+
+ @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]}
+
+ \noindent
+ We expect that the corresponding operator on finite sets, written @{term "fconcat"},
+ builds finite unions of finite sets:
+
+ @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
+
+ \noindent
+ The quotient package should automatically provide us with a definition for @{text "\<Union>"} in
+ terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is
+ that the method used in the existing quotient
+ packages of just taking the representation of the arguments and then taking
+ the abstraction of the result is \emph{not} enough. The reason is that in case
+ of @{text "\<Union>"} we obtain the incorrect definition
+
+ @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}
+
+ \noindent
+ where the right-hand side is not even typable! This problem can be remedied in the
+ existing quotient packages by introducing an intermediate step and reasoning
+ about flattening of lists of finite sets. However, this remedy is rather
+ cumbersome and inelegant in light of our work, which can deal with such
+ definitions directly. The solution is that we need to build aggregate
+ representation and abstraction functions, which in case of @{text "\<Union>"}
+ generate the following definition
+
+ @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat ((map_list Rep_fset \<circ> Rep_fset) S))"}
+
+ \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}.
+
+ In addition we are able to address the criticism by Paulson \cite{Paulson06} cited
+ at the beginning of this section about having to collect theorems that are
+ lifted from the raw level to the quotient level into one giant list. Homeier's and
+ also our quotient package are modular so that they allow lifting
+ theorems separately. This has the advantage for the user of being able to develop a
+ formal theory interactively as a natural progression. A pleasing side-result of
+ the modularity is that we are able to clearly specify what is involved
+ in the lifting process (this was only hinted at in \cite{Homeier05} and
+ implemented as a ``rough recipe'' in ML-code).
+
+
+ The paper is organised as follows: Section \ref{sec:prelims} presents briefly
+ some necessary preliminaries; Section \ref{sec:type} describes the definitions
+ of quotient types and shows how definitions of constants can be made over
+ quotient types. Section \ref{sec:resp} introduces the notions of respectfulness
+ and preservation; Section \ref{sec:lift} describes the lifting of theorems;
+ Section \ref{sec:examples} presents some examples
+ and Section \ref{sec:conc} concludes and compares our results to existing
+ work.
+*}
+
+section {* Preliminaries and General Quotients\label{sec:prelims} *}
+
+text {*
+ We 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 as follows
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}{@ {}rl@ {\hspace{3mm}}l@ {}}
+ @{text "\<sigma>, \<tau> ::="} & @{text "\<alpha> | (\<sigma>,\<dots>, \<sigma>) \<kappa>"} & (type variables and type constructors)\\
+ @{text "t, s ::="} & @{text "x\<^isup>\<sigma> | c\<^isup>\<sigma> | t t | \<lambda>x\<^isup>\<sigma>. t"} &
+ (variables, constants, applications and abstractions)\\
+ \end{tabular}
+ \end{isabelle}
+
+ \noindent
+ We often write just @{text \<kappa>} for @{text "() \<kappa>"}, and use @{text "\<alpha>s"} and
+ @{text "\<sigma>s"} to stand for collections of type variables and types,
+ respectively. The type of a term is often made explicit by writing @{text
+ "t :: \<sigma>"}. HOL includes a type @{typ bool} for booleans and the function
+ type, written @{text "\<sigma> \<Rightarrow> \<tau>"}. HOL also contains many primitive and defined
+ constants; 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
+
+ @{thm [display, indent=10] fun_map_def[no_vars, THEN eq_reflection]}
+
+ \noindent
+ Using this map-function, we can give the following, equivalent, but more
+ uniform definition for @{text add} shown in \eqref{adddef}:
+
+ @{text [display, indent=10] "add \<equiv> (Rep_int \<singlearr> Rep_int \<singlearr> Abs_int) add_pair"}
+
+ \noindent
+ Using extensionality and unfolding the definition 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>}. For a type @{text \<kappa>} with arguments @{text "\<alpha>\<^isub>1\<^isub>\<dots>\<^isub>n"} the
+ type of @{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
+ %
+ @{text [display, indent=10] "(R\<^isub>1 \<tripple> R\<^isub>2) (x\<^isub>1, x\<^isub>2) (y\<^isub>1, y\<^isub>2) \<equiv> R\<^isub>1 x\<^isub>1 y\<^isub>1 \<and> R\<^isub>2 x\<^isub>2 y\<^isub>2"}
+
+ \noindent
+ Homeier gives also the following operator for defining equivalence
+ relations over function types
+ %
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{thm fun_rel_def[of "R\<^isub>1" "R\<^isub>2", no_vars, 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 Quantification and Bounded Abstractions]\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) = 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{enumerate}
+ \item @{thm (rhs1) Quotient_def[of "R", no_vars]}
+ \item @{thm (rhs2) Quotient_def[of "R", no_vars]}
+ \item @{thm (rhs3) Quotient_def[of "R", no_vars]}
+ \end{enumerate}
+ \end{definition}
+
+ \noindent
+ The value of this definition lies in the fact that validity of @{text "Quotient R Abs Rep"} can
+ often be proved in terms of the validity of @{text "Quotient"} over the constituent
+ types of @{text "R"}, @{text Abs} and @{text Rep}.
+ For example Homeier proves the following property for higher-order quotient
+ types:
+
+ \begin{proposition}\label{funquot}
+ @{thm[mode=IfThen] fun_quotient[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"
+ and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]}
+ \end{proposition}
+
+ \noindent
+ As a result, Homeier is able to build an automatic prover that can nearly
+ always discharge a proof obligation involving @{text "Quotient"}. Our quotient
+ package makes heavy
+ use of this part of Homeier's work including an extension
+ for dealing with compositions of equivalence relations 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
+
+ @{text [display, indent=2] "Quotient (rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (Abs_fset \<circ> map_list Abs) (map_list Rep \<circ> Rep_fset)"}
+
+ \vspace{-.5mm}
+*}
+
+section {* Quotient Types and Quotient Definitions\label{sec:type} *}
+
+text {*
+ The first step in a quotient construction is to take a name for the new
+ type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},
+ defined over a raw type, say @{text "\<sigma>"}. The type of the equivalence
+ relation must be @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of
+ the quotient type declaration is therefore
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}\hfill\numbered{typedecl}
+ \end{isabelle}
+
+ \noindent
+ and a proof that @{text "R"} is indeed an equivalence relation. Two concrete
+ examples are
+
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}{@ {}l}
+ \isacommand{quotient\_type}~~@{text "int = nat \<times> nat / \<approx>\<^bsub>nat \<times> nat\<^esub>"}\\
+ \isacommand{quotient\_type}~~@{text "\<alpha> fset = \<alpha> list / \<approx>\<^bsub>list\<^esub>"}
+ \end{tabular}
+ \end{isabelle}
+
+ \noindent
+ which introduce the type of integers and of finite sets using the
+ equivalence relations @{text "\<approx>\<^bsub>nat \<times> nat\<^esub>"} and @{text
+ "\<approx>\<^bsub>list\<^esub>"} defined in \eqref{natpairequiv} and
+ \eqref{listequiv}, respectively (the proofs about being equivalence
+ relations is omitted). Given this data, we 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}
+ @{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.
+ \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}{rcl}
+ \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
+ @{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\
+ @{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\
+ \multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\
+ @{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
+ @{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
+ \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\
+ @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\
+ @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\
+ \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors with @{text "\<alpha>s
+ \<kappa>\<^isub>q"} being the quotient of the raw type @{text "\<rho>s \<kappa>"}:}\\
+ @{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 we rely 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"}). 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>"}. The
+ function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw
+ type as follows:
+ %
+ \begin{center}
+ \begin{tabular}{rcl}
+ @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a\<^sup>\<alpha>"}\\
+ @{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id :: \<kappa> \<Rightarrow> \<kappa>"}\\
+ @{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\
+ @{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>as. MAP'(\<sigma>)"}
+ \end{tabular}
+ \end{center}
+ %
+ \noindent
+ In this definition we rely on the fact that 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.
+
+ @{text [display, indent=10] "\<lambda>a b. map_prod (map_list a) b"}
+
+ \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
+
+ @{text [display, indent=10] "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map_list id"}
+
+ \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
+
+ @{text [display, indent=10] "(map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
+
+ \noindent
+ which we can use for defining @{term "fconcat"} as follows
+
+ @{text [display, indent=10] "\<Union> \<equiv> ((map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}
+
+ \noindent
+ Note that by using the operator @{text "\<singlearr>"} and special clauses
+ for function types in \eqref{ABSREP}, we do not have to
+ distinguish between arguments and results, but can deal with them uniformly.
+ Consequently, all definitions in the quotient package
+ are of the general form
+
+ @{text [display, indent=10] "c \<equiv> ABS (\<sigma>, \<tau>) t"}
+
+ \noindent
+ where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the
+ type of the defined quotient constant @{text "c"}. This data can be easily
+ generated from the declaration given by the user.
+ To increase the confidence in this way of making definitions, we can prove
+ that the terms involved are all typable.
+
+ \begin{lemma}
+ If @{text "ABS (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"}
+ and @{text "REP (\<sigma>, \<tau>)"} some representation function @{text "Rep"},
+ then @{text "Abs"} is of type @{text "\<sigma> \<Rightarrow> \<tau>"} and @{text "Rep"} of type
+ @{text "\<tau> \<Rightarrow> \<sigma>"}.
+ \end{lemma}
+
+ \begin{proof}
+ By mutual induction and analysing the definitions of @{text "ABS"} 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 {*
+ 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}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "bn (x) \<equiv> \<emptyset>"}\hspace{4mm}
+ @{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{4mm}
+ @{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}
+ \end{isabelle}
+
+ \noindent
+ 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}{rcl}
+ \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
+ @{text "REL (\<sigma>, \<sigma>)"} & $\dn$ & @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
+ \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\
+ @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
+ \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors with @{text "\<alpha>s
+ \<kappa>\<^isub>q"} being the quotient of the raw type @{text "\<rho>s \<kappa>"}:}\smallskip\\
+ @{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}:
+ 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
+
+ @{text [display, indent=10] "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
+
+ \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
+
+ @{text [display, indent=10] "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
+
+ \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
+
+ @{text [display, indent=10] "\<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)"}
+
+ \noindent
+ In contrast, if we lift a theorem about @{text "append"} to a theorem describing
+ the union of finite sets, then we need to discharge the proof obligation
+
+ @{text [display, indent=10] "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}
+
+ \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
+
+ @{text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"}
+
+ \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
+
+ @{text [display, indent=10] "(Rep ---> map_list Rep ---> map_list Abs) cons = cons"}
+
+ \noindent
+ under the assumption @{text "Quotient R Abs Rep"}. Interestingly, 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 the corresponding preservation property.
+
+ %%%@ {thm [display, indent=10] insert_preserve2[no_vars]}
+
+ %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
+
+ 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.
+
+ 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.
+ In contrast to other quotient packages, our package requires that the user specifies
+ both, the @{text "raw_thm"} (as theorem) and the \emph{term} of the @{text "quot_thm"}.\footnote{Though we
+ also provide a fully automated mode, where the @{text "quot_thm"} is guessed
+ from the form of @{text "raw_thm"}.} As a result, the user has fine control
+ over which parts of a raw theorem should be lifted.
+
+ 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.
+
+ 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 simultaneously recursing on
+ the structure of @{text "raw_thm"} and @{text "quot_thm"} as follows:
+
+ \begin{center}
+ \begin{tabular}{rcl}
+ \multicolumn{3}{@ {}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> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
+ \end{cases}$\smallskip\\
+ \\
+ \multicolumn{3}{@ {}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> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
+ \end{cases}$\smallskip\\
+ \multicolumn{3}{@ {}l}{equality:}\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{3}{@ {}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}{rcl}
+ \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions:}\\
+ @{text "INJ (\<lambda>x. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$ &
+ $\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}$\\
+ @{text "INJ (\<lambda>x \<in> R. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$
+ & @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x \<in> R. INJ (t, s)))"}\smallskip\\
+ \multicolumn{3}{@ {\hspace{-4mm}}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{3}{@ {\hspace{-4mm}}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 proof step, 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. In this case we have
+ rules of the form
+
+ @{text [display, indent=10] "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}
+
+ \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
+
+ @{text [display, indent=10] "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}
+
+ \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?
+
+ @{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
+
+ \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 proof step, 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 and is defined for a goal being a relation between these two terms.
+
+ \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:
+
+ @{term [display, indent=10] "R x y \<longrightarrow> R x (Rep (Abs y))"}
+
+ Otherwise we introduce an appropriate relation between the subterms
+ and continue with two subgoals using the lemma:
+
+ @{text [display, indent=10] "(R\<^isub>1 \<doublearr> R\<^isub>2) f g \<longrightarrow> R\<^isub>1 x y \<longrightarrow> R\<^isub>2 (f x) (g y)"}
+ \end{itemize}
+
+ We defined the theorem @{text "inj_thm"} in such a way that
+ establishing the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be
+ achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient
+ definitions. First the definitions of all lifted constants
+ are used to fold the @{term Rep} with the raw constants. 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:
+
+ @{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
+
+ \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}:
+
+ @{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]}
+
+ \noindent
+ Finally, we rewrite with the preservation theorems. This will result
+ in two equal terms that can be solved by reflexivity.
+ *}
+
+
+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...
+
+ In this section 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> (nat \<times> nat)"}\\
+ \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 [display, indent=10] "0 + x = x"}
+
+ \noindent
+ 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}).
+*}
+
+section {* Conclusion and Related Work\label{sec:conc}*}
+
+text {*
+
+ The code of the quotient package and the examples described here are already
+ included in the standard distribution of Isabelle.\footnote{Available from
+ \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} 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}.
+
+
+ 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
+%%
+ \medskip
+
+ \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.
+
+*}
+
+
+
+(*<*)
+end
+(*>*)