(*<*)
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
(*>*)