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