(* How to change the notation for \<lbrakk> \<rbrakk> meta-level implications? *)

(*<*)
theory Paper
imports "Quotient"
        "LaTeXsugar"
        "../Nominal/FSet"
begin

notation (latex output)
  rel_conj ("_ OOO _" [53, 53] 52) and
  "op -->" (infix "\<rightarrow>" 100) and
  "==>" (infix "\<Rightarrow>" 100) and
  fun_map ("_ \<^raw:\mbox{\singlearr}> _" 51) and
  fun_rel ("_ \<^raw:\mbox{\doublearr}> _" 51) and
  list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
  fempty ("\<emptyset>") and
  funion ("_ \<union> _") and
  finsert ("{_} \<union> _") and 
  Cons ("_::_") and
  concat ("flat") and
  fconcat ("\<Union>")
 
  

ML {*
fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;
fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
  let
    val concl =
      Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)
  in
    case concl of (_ $ l $ r) => proj (l, r)
    | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
  end);
*}
setup {*
  Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #>
  Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #>
  Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))
*}
(*>*)


section {* Introduction *}

text {* 
   \begin{flushright}
  {\em ``Not using a [quotient] package has its advantages: we do not have to\\ 
    collect all the theorems we shall ever want into one giant list;''}\\
    Larry Paulson \cite{Paulson06}
  \end{flushright}\smallskip

  \noindent
  Isabelle is a popular generic theorem prover in which many logics can be
  implemented. The most widely used one, however, is Higher-Order Logic
  (HOL). This logic consists of a small number of axioms and inference rules
  over a simply-typed term-language. Safe reasoning in HOL is ensured by two
  very restricted mechanisms for extending the logic: one is the definition of
  new constants in terms of existing ones; the other is the introduction of
  new types by identifying non-empty subsets in existing types. It is well
  understood how to use both mechanisms for dealing with quotient
  constructions in HOL (see \cite{Homeier05,Paulson06}).  For example the
  integers in Isabelle/HOL are constructed by a quotient construction over the
  type @{typ "nat \<times> nat"} and the equivalence relation

  @{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + m\<^isub>2 = m\<^isub>1 + n\<^isub>2"}

  \noindent
  This constructions yields the new type @{typ int} and definitions for @{text
  "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of
  natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations
  such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in
  terms of operations on pairs of natural numbers (namely @{text
  "add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2,
  m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}).
  Similarly one can construct the type of finite sets, written @{term "\<alpha> fset"}, 
  by quotienting the type @{text "\<alpha> list"} according to the equivalence relation

  @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}

  \noindent
  which states that two lists are equivalent if every element in one list is
  also member in the other. The empty finite set, written @{term "{||}"}, can
  then be defined as the empty list and the union of two finite sets, written
  @{text "\<union>"}, as list append.

  An area where quotients are ubiquitous is reasoning about programming language
  calculi. A simple example is the lambda-calculus, whose raw terms are defined as

  @{text [display, indent=10] "t ::= x | t t | \<lambda>x.t"}

  \noindent
  The problem with this definition arises when one attempts to
  prove formally, for example, the substitution lemma \cite{Barendregt81} by induction
  over the structure of terms. This can be fiendishly complicated (see
  \cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof
  about raw lambda-terms). In contrast, if we reason about
  $\alpha$-equated lambda-terms, that means terms quotient according to
  $\alpha$-equivalence, then the reasoning infrastructure provided, 
  for example, by Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal 
  proof of the substitution lemma almost trivial. 

  The difficulty is that in order to be able to reason about integers, finite
  sets or $\alpha$-equated lambda-terms one needs to establish a reasoning
  infrastructure by transferring, or \emph{lifting}, definitions and theorems
  from the raw type @{typ "nat \<times> nat"} to the quotient type @{typ int}
  (similarly for finite sets and $\alpha$-equated lambda-terms). This lifting
  usually requires a \emph{lot} of tedious reasoning effort \cite{Paulson06}.  
  It is feasible to to this work manually, if one has only a few quotient
  constructions at hand. But if they have to be done over and over again as in 
  Nominal Isabelle, then manual reasoning is not an option.

  The purpose of a \emph{quotient package} is to ease the lifting of theorems
  and automate the definitions and reasoning as much as possible. In the
  context of HOL, there have been a few quotient packages already
  \cite{harrison-thesis,Slotosch97}. The most notable 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, often referred to as the \emph{raw
  type}, 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 they need to be derived from slightly
  more basic functions. We will show the details later. } These functions
  relate elements in the existing type to ones in the new type and vice versa;
  they can be uniquely identified by their type. For example for the integer
  quotient construction the types of @{text Abs} and @{text Rep} are

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  @{text "Abs :: nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep :: int \<Rightarrow> nat \<times> nat"}
  \end{isabelle}

  \noindent
  However we often leave this typing information implicit for better
  readability, but sometimes 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 (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs (1, 0)"}
  \end{isabelle}

  \noindent
  Slightly more complicated is the definition of @{text "add"} having type 
  @{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition is as follows

  @{text [display, indent=10] "add n m \<equiv> Abs (add_pair (Rep n) (Rep m))"}
  
  \noindent
  where we take the representation of the arguments @{text n} and @{text m},
  add them according to the function @{text "add_pair"} and then take the
  abstraction of the result.  This is all straightforward and the existing
  quotient packages can deal with such definitions. But what is surprising
  that none of them can deal with slightly more complicated definitions involving
  \emph{compositions} of quotients. Such compositions are needed for example
  in case of quotienting lists to obtain finite sets and the operator that 
  flattens lists of lists, defined as follows

  @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]}

  \noindent
  We expect that the corresponding operator on finite sets, written @{term "fconcat"},
  builds the union of finite sets of finite sets:

  @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}

  \noindent
  The quotient package should provide us with a definition for @{text "\<Union>"} in
  terms of @{text flat}, @{text Rep} and @{text Abs} (the latter two having
  the type @{text "\<alpha> fset \<Rightarrow> \<alpha> list"} and @{text "\<alpha> list \<Rightarrow> \<alpha> fset"},
  respectively). The problem is that the method  used in the existing quotient
  packages of just taking the representation of the arguments and then take
  the abstraction of the result is \emph{not} enough. The reason is that case in case
  of @{text "\<Union>"} we obtain the incorrect definition

  @{text [display, indent=10] "\<Union> S \<equiv> Abs_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 relation}, \emph{respectfulness} and \emph{preservation}
  from Homeier \cite{Homeier05}.

  We will also address the criticism by Paulson \cite{Paulson06} cited at the
  beginning of this section about having to collect theorems that are lifted from the raw
  level to the quotient level. Our quotient package is the first one that is modular so that it
  allows to lift single theorems separately. This has the advantage for the
  user to develop a formal theory interactively an a natural progression. A
  pleasing result of the modularity is also that we are able to clearly
  specify what needs to be done in the lifting process (this was only hinted at in
  \cite{Homeier05} and implemented as a ``rough recipe'' in ML-code).
 
  The paper is organised as follows \ldots
*}



section {* Preliminaries and General Quotient\label{sec:prelims} *}



text {*
  In this section we present the definitions of a quotient that follow
  those by Homeier, the proofs can be found there.

  \begin{definition}[Quotient]
  A relation $R$ with an abstraction function $Abs$
  and a representation function $Rep$ is a \emph{quotient}
  if and only if:

  \begin{enumerate}
  \item @{thm (rhs1) Quotient_def[of "R", no_vars]}
  \item @{thm (rhs2) Quotient_def[of "R", no_vars]}
  \item @{thm (rhs3) Quotient_def[of "R", no_vars]}
  \end{enumerate}

  \end{definition}

  \begin{definition}[Relation map and function map]\\
  @{thm fun_rel_def[of "R1" "R2", no_vars]}\\
  @{thm fun_map_def[no_vars]}
  \end{definition}

  The main theorems for building higher order quotients is:
  \begin{lemma}[Function Quotient]
  If @{thm (prem 1) fun_quotient[no_vars]} and @{thm (prem 2) fun_quotient[no_vars]}
  then @{thm (concl) fun_quotient[no_vars]}
  \end{lemma}

*}

subsection {* Higher Order Logic *}

text {*

  Types:
  \begin{eqnarray}\nonumber
  @{text "\<sigma> ::="} & @{text "\<alpha>"} & \textrm{(type variable)} \\ \nonumber
      @{text "|"} & @{text "(\<sigma>,\<dots>,\<sigma>)\<kappa>"} & \textrm{(type construction)}
  \end{eqnarray}

  Terms:
  \begin{eqnarray}\nonumber
  @{text "t ::="} & @{text "x\<^isup>\<sigma>"} & \textrm{(variable)} \\ \nonumber
      @{text "|"} & @{text "c\<^isup>\<sigma>"} & \textrm{(constant)} \\ \nonumber
      @{text "|"} & @{text "t t"} & \textrm{(application)} \\ \nonumber
      @{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber
  \end{eqnarray}

  {\it Say more about containers / maping functions }

*}

section {* Quotient Types and Lifting of Definitions *}

text {*
  The first step in a quotient constructions is to take a name for the new
  type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation defined over a
  raw type, say @{text "\<sigma>"}. The equivalence relation for the quotient
  construction, lets say @{text "R"}, must then be of type @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
  bool"}. The user-visible part of the declaration is therefore 

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}
  \end{isabelle}

  \noindent
  and a proof that @{text "R"} is indeed an equivalence relation.
  Given this data, we can internally declare the quotient type as
  
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \isacommand{typedef}~~@{text "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>x. c = R x}"}
  \end{isabelle}

  \noindent
  being the (non-empty) set of equivalence classes of @{text "R"}. The
  restriction 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 provide us with abstraction and
  representation functions having the type

  \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 
  and relating 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

  @{text [display, indent=10] "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}

  \noindent
  holds (for the proof see \cite{Homeier05}).

  The next step is to lift definitions over the raw type to definitions over the
  quotient type. For this we provide the declaration

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~\isacommand{is}~@{text "c' :: \<sigma>"}
  \end{isabelle}

  To define a constant on the lifted type, an aggregate abstraction
  function is applied to the raw constant. Below we describe the operation
  that generates
  an aggregate @{term "Abs"} or @{term "Rep"} function given the
  compound raw type and the compound quotient type.
  This operation will also be used in translations of theorem statements
  and in the lifting procedure.

  The operation is additionally able to descend into types for which
  maps are known. Such maps for most common types (list, pair, sum,
  option, \ldots) are described in Homeier, and we assume that @{text "map"}
  is the function that returns a map for a given type. Then REP/ABS is defined
  as follows:

  {\it the first argument is the raw type and the second argument the quotient type}
  %
  \begin{center}
  \begin{longtable}{rcl}
  \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ 
  @{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\\
  @{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\smallskip\\
  \multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\ 
  @{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
  @{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
  \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\ 
  @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "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{longtable}
  \end{center}
  %
  \noindent
  where in the last two clauses we have that the quotient type @{text "\<alpha>s \<kappa>\<^isub>q"} is a quotient of
  the raw type @{text "\<rho>s \<kappa>"} (for example @{text "\<alpha> fset"} and @{text "\<alpha> list"}). 
  The quotient construction ensures that the type variables in @{text "\<rho>s"} 
  must be amongst the @{text "\<alpha>s"}. Now the @{text "\<sigma>s'"} are given by the matchers 
  for the @{text "\<alpha>s"} 
  when matching  @{text "\<sigma>s \<kappa>\<^isub>q"} against @{text "\<alpha>s \<kappa>\<^isub>q"}; similarly the @{text "\<tau>s'"} are given by the 
  same type-variables when matching @{text "\<tau>s \<kappa>"} against @{text "\<rho>s \<kappa>"}.
  The function @{text "MAP"} calculates an \emph{aggregate map-function} for a type 
  as follows:

  \begin{center}
  \begin{tabular}{rcl}
  @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a"}\\
  @{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id"}\\
  @{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 abuse the fact that we can interpret type-variables @{text \<alpha>} as 
  term variables @{text a}, and in the last clause build an abstraction over all
  term-variables inside the aggregate map-function generated by @{text "MAP'"}.
  This aggregate map-function is necessary if we build quotients, say @{text "(\<alpha>, \<beta>) foo"},
  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
  Returning to our example about @{term "concat"} and @{term "fconcat"} which have the
  types @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}. Feeding this
  into @{text ABS} gives us the abstraction function:

  @{text [display, indent=10] "(map (map id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map id"}

  \noindent
  where we already performed some @{text "\<beta>"}-simplifications. In our implementation
  we further simplified this by noticing 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 simplified 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"}

  Apart from the last 2 points the definition is same as the one implemented in
  in Homeier's HOL package. Adding composition in last two cases is necessary
  for compositional quotients. We illustrate the different behaviour of the
  definition by showing the derived definition of @{term fconcat}:

  @{thm fconcat_def[no_vars]}

  The aggregate @{term Abs} function takes a finite set of finite sets
  and applies @{term "map rep_fset"} composed with @{term rep_fset} to
  its input, obtaining a list of lists, passes the result to @{term concat}
  obtaining a list and applies @{term abs_fset} obtaining the composed
  finite set.

  For every type map function we require the property that @{term "map id = id"}.
  With this we can compactify the term, removing the identity mappings,
  obtaining a definition that is the same as the one provided by Homeier
  in the cases where the internal type does not change.

  {\it we should be able to prove}

  \begin{lemma}
  If @{text "ABS (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"} 
  and @{text "REP (\<sigma>, \<tau>)"} some representation function @{text "Rep"}, 
  then @{text "Abs"} is of type @{text "\<sigma> \<Rightarrow> \<tau>"} and @{text "Rep"} of type
  @{text "\<tau> \<Rightarrow> \<sigma>"}.
  \end{lemma}

  This lemma fails in the over-simplified abstraction and representation function used
  in Homeier's quotient package.
*}

subsection {* Respectfulness *}

text {*

  A respectfulness lemma for a constant states that the equivalence
  class returned by this constant depends only on the equivalence
  classes of the arguments applied to the constant. To automatically
  lift a theorem that talks about a raw constant, to a theorem about
  the quotient type a respectfulness theorem is required.

  A respectfulness condition for a constant can be expressed in
  terms of an aggregate relation between the constant and itself,
  for example the respectfullness for @{term "append"}
  can be stated as:

  @{thm [display, indent=10] append_rsp[no_vars]}

  \noindent
  Which after unfolding the definition of @{term "op ===>"} is equivalent to:

  @{thm [display, indent=10] append_rsp_unfolded[no_vars]}

  \noindent An aggregate relation is defined in terms of relation
  composition, so we define it first:

  \begin{definition}[Composition of Relations]
  @{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate
  composition @{thm pred_compI[no_vars]}
  \end{definition}

  The aggregate relation for an aggregate raw type and quotient type
  is defined as:

  \begin{itemize}
  \item @{text "REL(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "op ="}
  \item @{text "REL(\<sigma>, \<sigma>)"}  =  @{text "op ="}
  \item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(rel \<kappa>) (REL(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REL(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
  \item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "(rel \<kappa>\<^isub>1) (REL(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REL(\<rho>\<^isub>p,\<nu>\<^isub>p) OOO Eqv_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}

  \end{itemize}

  Again, the last case is novel, so lets look at the example of
  respectfullness for @{term concat}. The statement according to
  the definition above is:

  @{thm [display, indent=10] concat_rsp[no_vars]}

  \noindent
  By unfolding the definition of relation composition and relation map
  we can see the equivalent statement just using the primitive list
  equivalence relation:

  @{thm [display, indent=10] concat_rsp_unfolded[of "a" "a'" "b'" "b", no_vars]}

  The statement reads that, for any lists of lists @{term a} and @{term b}
  if there exist intermediate lists of lists @{term "a'"} and @{term "b'"}
  such that each element of @{term a} is in the relation with an appropriate
  element of @{term a'}, @{term a'} is in relation with @{term b'} and each
  element of @{term b'} is in relation with the appropriate element of
  @{term b}.

*}

subsection {* Preservation *}

text {*
  Sometimes a non-lifted polymorphic constant is instantiated to a
  type being lifted. For example take the @{term "op #"} which inserts
  an element in a list of pairs of natural numbers. When the theorem
  is lifted, the pairs of natural numbers are to become integers, but
  the head constant is still supposed to be the head constant, just
  with a different type.  To be able to lift such theorems
  automatically, additional theorems provided by the user are
  necessary, we call these \emph{preservation} theorems following
  Homeier's naming.

  To lift theorems that talk about insertion in lists of lifted types
  we need to know that for any quotient type with the abstraction and
  representation functions @{text "Abs"} and @{text Rep} we have:

  @{thm [display, indent=10] (concl) cons_prs[no_vars]}

  This is not enough to lift theorems that talk about quotient compositions.
  For some constants (for example empty list) it is possible to show a
  general compositional theorem, but for @{term "op #"} it is necessary
  to show that it respects the particular quotient type:

  @{thm [display, indent=10] insert_preserve2[no_vars]}
*}

subsection {* Composition of Quotient theorems *}

text {*
  Given two quotients, one of which quotients a container, and the
  other quotients the type in the container, we can write the
  composition of those quotients. To compose two quotient theorems
  we compose the relations with relation composition as defined above
  and the abstraction and relation functions are the ones of the sub
  quotients composed with the usual function composition.
  The @{term "Rep"} and @{term "Abs"} functions that we obtain agree
  with the definition of aggregate Abs/Rep functions and the
  relation is the same as the one given by aggregate relations.
  This becomes especially interesting
  when we compose the quotient with itself, as there is no simple
  intermediate step.

  Lets take again the example of @{term concat}. To be able to lift
  theorems that talk about it we provide the composition quotient
  theorems, which then lets us perform the lifting procedure in an
  unchanged way:

  @{thm [display] quotient_compose_list[no_vars]}
*}


section {* Lifting of Theorems *}

text {*
  The core of the quotient package takes an original theorem that
  talks about the raw types, and the statement of the theorem that
  it is supposed to produce. This is different from other existing
  quotient packages, where only the raw theorems were necessary.
  We notice that in some cases only some occurrences of the raw
  types need to be lifted. This is for example the case in the
  new Nominal package, where a raw datatype that talks about
  pairs of natural numbers or strings (being lists of characters)
  should not be changed to a quotient datatype with constructors
  taking integers or finite sets of characters. To simplify the
  use of the quotient package we additionally provide an automated
  statement translation mechanism that replaces occurrences of
  types that match given quotients by appropriate lifted types.

  Lifting the theorems is performed in three steps. In the following
  we call these steps \emph{regularization}, \emph{injection} and
  \emph{cleaning} following the names used in Homeier's HOL
  implementation.

  We first define the statement of the regularized theorem based
  on the original theorem and the goal theorem. Then we define
  the statement of the injected theorem, based on the regularized
  theorem and the goal. We then show the 3 proofs, as all three
  can be performed independently from each other.

*}

subsection {* Regularization and Injection statements *}

text {*

  We first define the function @{text REG}, which takes the statements
  of the raw theorem and the lifted theorem (both as terms) and
  returns the statement of the regularized version. The intuition
  behind this function is that it replaces quantifiers and
  abstractions involving raw types by bounded ones, and equalities
  involving raw types are replaced by appropriate aggregate
  relations. It is defined as follows:

  \begin{itemize}
  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"}
  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"}
  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
  \item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"}
  \item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"}
  \item @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}
  \item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"}
  \item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"}
  \end{itemize}

  In the above definition we 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{itemize}
  \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"}
  \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"}
  \item @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"}
  \item @{text "INJ (\<forall> t, \<forall> s) = \<forall> (INJ (t, s)"}
  \item @{text "INJ (\<forall> t \<in> R, \<forall> s) = \<forall> (INJ (t, s) \<in> R"}
  \item @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}
  \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) = v\<^isub>1"}
  \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"}
  \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) = c\<^isub>1"}
  \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"}
  \end{itemize}

  For existential quantifiers and unique existential quantifiers it is
  defined similarly to the universal one.

*}

subsection {* Proof procedure *}

(* In the below the type-guiding 'QuotTrue' assumption is removed; since we
   present in a paper a version with typed-variables it is not necessary *)

text {*

  With the above definitions of @{text "REG"} and @{text "INJ"} we can show
  how the proof is performed. The first step is always the application of
  of the following lemma:

  @{term [display, indent=10] "[|A; A --> B; B = C; C = D|] ==> D"}

  With @{text A} instantiated to the original raw theorem, 
       @{text B} instantiated to @{text "REG(A)"},
       @{text C} instantiated to @{text "INJ(REG(A))"},
   and @{text D} instantiated to the statement of the lifted theorem.
  The first assumption can be immediately discharged using the original
  theorem and the three left subgoals are exactly the subgoals of regularization,
  injection and cleaning. The three can be proved independently by the
  framework and in case there are non-solved subgoals they can be left
  to the user.

  The injection and cleaning subgoals are always solved if the appropriate
  respectfulness and preservation theorems are given. It is not the case
  with regularization; sometimes a theorem given by the user does not
  imply a regularized version and a stronger one needs to be proved. This
  is outside of the scope of the quotient package, so the user is then left
  with such obligations. As an example lets see the simplest possible
  non-liftable theorem for integers: When we want to prove @{term "0 \<noteq> 1"}
  on integers the fact that @{term "\<not> (0, 0) = (1, 0)"} is not enough. It
  only shows that particular items in the equivalence classes are not equal,
  a more general statement saying that the classes are not equal is necessary.
*}

subsection {* Proving Regularization *}

text {*

  Isabelle provides a set of \emph{mono} rules, that are used to split implications
  of similar statements into simpler implication subgoals. These are enhanced
  with special quotient theorem in the regularization goal. Below we only show
  the versions for the universal quantifier. For the existential quantifier
  and abstraction they are analogous with some symmetry.

  First, bounded universal quantifiers can be removed on the right:

  @{thm [display, indent=10] ball_reg_right[no_vars]}

  They can be removed anywhere if the relation is an equivalence relation:

  @{thm [display, indent=10] ball_reg_eqv[no_vars]}

  And finally it can be removed anywhere if @{term R2} is an equivalence relation, then:

  @{thm [display, indent=10] (concl) ball_reg_eqv_range[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 useful. We use it 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.

*}

(*
  @{thm bex_reg_eqv_range[no_vars]}
  @{thm [display] bex_reg_left[no_vars]}
  @{thm [display] bex1_bexeq_reg[no_vars]}
  @{thm [display] bex_reg_eqv[no_vars]}
  @{thm [display] babs_reg_eqv[no_vars]}
  @{thm [display] babs_simp[no_vars]}
*)

subsection {* Injection *}

text {*
  The injection proof starts with an equality between the regularized theorem
  and the injected version. The proof again follows by the structure of the
  two term, and is defined for a goal being a relation between the two terms.

  \begin{itemize}
  \item For two constants, an appropriate constant respectfullness assumption is used.
  \item For two variables, the regularization assumptions state that they are related.
  \item For two abstractions, they are eta-expanded and beta-reduced.
  \end{itemize}

  Otherwise the two terms are applications. There are two cases: If there is a REP/ABS
  in the injected theorem we can use the theorem:

  @{thm [display] rep_abs_rsp[no_vars]}

  and continue the proof.

  Otherwise we introduce an appropriate relation between the subterms and continue with
  two subgoals using the lemma:

  @{thm [display] apply_rsp[no_vars]}

*}

subsection {* Cleaning *}

text {*
  The @{text REG} and @{text INJ} functions have been defined in such a way
  that establishing the goal theorem now consists only on rewriting the
  injected theorem with the preservation theorems.

  \begin{itemize}
  \item First for lifted constants, their definitions are the preservation rules for
    them.
  \item For lambda abstractions lambda preservation establishes
    the equality between the injected theorem and the goal. This allows both
    abstraction and quantification over lifted types.
    @{thm [display] lambda_prs[no_vars]}
  \item Relations over lifted types are folded with:
    @{thm [display] Quotient_rel_rep[no_vars]}
  \item User given preservation theorems, that allow using higher level operations
    and containers of types being lifted. An example may be
    @{thm [display] map_prs(1)[no_vars]}
  \end{itemize}

 Preservation of relations and user given constant preservation lemmas *}

section {* Examples *}

(* Mention why equivalence *)

text {*

  A user of our quotient package first needs to define an equivalence relation:

  @{text "fun \<approx> where (x, y) \<approx> (u, v) = (x + v = u + y)"}

  Then the user defines a quotient type:

  @{text "quotient_type int = (nat \<times> nat) / \<approx>"}

  Which leaves a proof obligation that the relation is an equivalence relation,
  that can be solved with the automatic tactic with two definitions.

  The user can then specify the constants on the quotient type:

  @{text "quotient_definition 0 \<Colon> int is (0\<Colon>nat, 0\<Colon>nat)"}
  @{text "fun plus_raw where plus_raw (x, y) (u, v) = (x + u, y + v)"}
  @{text "quotient_definition (op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int) is plus_raw"}

  Lets first take a simple theorem about addition on the raw level:

  @{text "lemma plus_zero_raw: plus_raw (0, 0) i \<approx> i"}

  When the user tries to lift a theorem about integer addition, the respectfulness
  proof obligation is left, so let us prove it first:
  
  @{text "lemma (op \<approx> \<Longrightarrow> op \<approx> \<Longrightarrow> op \<approx>) plus_raw plus_raw"}

  Can be proved automatically by the system just by unfolding the definition
  of @{term "op \<Longrightarrow>"}.

  Now the user can either prove a lifted lemma explicitly:

  @{text "lemma 0 + i = i by lifting plus_zero_raw"}

  Or in this simple case use the automated translation mechanism:

  @{text "thm plus_zero_raw[quot_lifted]"}

  obtaining the same result.
*}

section {* Related Work *}

text {*
  \begin{itemize}

  \item Peter Homeier's package~\cite{Homeier05} (and related work from there)
  \item John Harrison's one~\cite{harrison-thesis} is the first one to lift theorems
    but only first order.

  \item PVS~\cite{PVS:Interpretations}
  \item MetaPRL~\cite{Nogin02}
  \item Manually defined quotients in Isabelle/HOL Library (Markus's Quotient\_Type,
    Dixon's FSet, \ldots)

  \item Oscar Slotosch defines quotient-type automatically but no
    lifting~\cite{Slotosch97}.

  \item PER. And how to avoid it.

  \item Necessity of Hilbert Choice op and Larry's quotients~\cite{Paulson06}

  \item Setoids in Coq and \cite{ChicliPS02}

  \end{itemize}
*}

section {* Conclusion *}

text {*
  The package is part of the standard distribution of Isabelle.
*}


subsection {* Contributions *}

text {*
  We present the detailed lifting procedure, which was not shown before.

  The quotient package presented in this paper has the following
  advantages over existing packages:
  \begin{itemize}

  \item We define quotient composition, function map composition and
    relation map composition. This lets lifting polymorphic types with
    subtypes quotiented as well. We extend the notions of
    respectfulness and preservation to cope with quotient
    composition.

  \item We allow lifting only some occurrences of quotiented
    types. Rsp/Prs extended. (used in nominal)

  \item The quotient package is very modular. Definitions can be added
    separately, rsp and prs can be proved separately, Quotients and maps
    can be defined separately and theorems can
    be lifted on a need basis. (useful with type-classes).

  \item Can be used both manually (attribute, separate tactics,
    rsp/prs databases) and programatically (automated definition of
    lifted constants, the rsp proof obligations and theorem statement
    translation according to given quotients).

  \end{itemize}
*}



(*<*)
end
(*>*)