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

notation (latex output)
  rel_conj ("_ OOO _" [53, 53] 52)
and
  fun_map ("_ ---> _" [51, 51] 50)
and
  fun_rel ("_ ===> _" [51, 51] 50)
and
  list_eq (infix "\<approx>" 50) (* Not sure if we want this notation...? *)

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 {* 
  {\hfill quote by Larry}\bigskip

  \noindent
  Isabelle is a 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 
  to use both mechanism for dealing with quotient constructions in HOL (cite Larry).
  For example the integers in Isabelle/HOL are constructed by a quotient construction over 
  the type @{typ "nat \<times> nat"} and the equivalence relation

% I would avoid substraction for natural numbers.

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

  \noindent
  Similarly one can construct the type of finite sets by quotienting lists
  according to the equivalence relation

  @{text [display] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}

  \noindent
  where @{text "\<in>"} stands for membership in a list.

  The problem is that in order to start reasoning about, for example integers, 
  definitions and theorems need to be transferred, or \emph{lifted}, 
  from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int}. 
  This lifting usually requires a lot of tedious reasoning effort.
  The purpose of a \emph{quotient package} is to ease the lifting and automate
  the reasoning involved as much as possible. Such a package is a central
  component of the new version of Nominal Isabelle where representations 
  of alpha-equated terms are constructed according to specifications given by
  the user. 
  
  In the context of HOL, there have been several quotient packages (...). The
  most notable is the one by Homeier (...) implemented in HOL4. However, what is
  surprising, none of them can deal compositions of quotients, for example with 
  lifting theorems about @{text "concat"}:

  @{thm [display] concat.simps(1)}
  @{thm [display] concat.simps(2)[no_vars]}

  \noindent
  One would like to lift this definition to the operation:

  @{thm [display] fconcat_empty[no_vars]}
  @{thm [display] fconcat_insert[no_vars]}

  \noindent
  What is special about this operation is that we have as input
  lists of lists which after lifting turn into finite sets of finite
  sets.
*}

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 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}
*}

section {* Quotient Type*}



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}

*}

section {* Constants *}

(* Say more about containers? *)

text {*

  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:

  \begin{itemize}
  \item @{text "ABS(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "id"}
  \item @{text "REP(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"}  =  @{text "id"}
  \item @{text "ABS(\<sigma>, \<sigma>)"}  =  @{text "id"}
  \item @{text "REP(\<sigma>, \<sigma>)"}  =  @{text "id"}
  \item @{text "ABS(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "REP(\<sigma>\<^isub>1,\<tau>\<^isub>1) ---> ABS(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
  \item @{text "REP(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1) ---> REP(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
  \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(map \<kappa>) (ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (ABS(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
  \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(map \<kappa>) (REP(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REP(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
  \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "Abs_\<kappa>\<^isub>2 \<circ> (map \<kappa>\<^isub>1) (ABS(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (ABS(\<rho>\<^isub>p,\<nu>\<^isub>p)"} 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"}
  \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "(map \<kappa>\<^isub>1) (REP(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REP(\<rho>\<^isub>p,\<nu>\<^isub>p) \<circ> Rep_\<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}

  Apart from the last 2 points the definition is same as the one implemented in
  in Homeier's HOL package, below is the definition of @{term fconcat}
  that shows the last points:

  @{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.
*}

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. This 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] append_rsp[no_vars]}

  \noindent
  Which is equivalent to:

  @{thm [display] append_rsp_unfolded[no_vars]}

  Below we show the algorithm for finding the aggregate relation.
  This algorithm uses
  the relation composition which we define as:

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

  Given an aggregate raw type and quotient type:

  \begin{itemize}
  \item For equal types or free type variables return equality

  \item For equal type constructors use the appropriate rel
    function applied to the results for the argument pairs

  \item For unequal type constructors, look in the quotients information
    for a quotient type that matches the type constructor, and instantiate
    the type appropriately getting back an instantiation environment. We
    apply the environment to the arguments and recurse composing it with
    the aggregate relation function.

  \end{itemize}

  Again, the the behaviour of our algorithm in the last situation is
  novel, so lets look at the example of respectfullness for @{term concat}.
  The statement as computed by the algorithm above is:

  @{thm [display] 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] 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 {*
  To be able to lift theorems that talk about constants that are not
  lifted but whose type changes when lifting is performed additionally
  preservation theorems are needed.

  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] (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] 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
  and the abstraction and relation functions with function composition.
  The @{term "Rep"} and @{term "Abs"} functions that we obtain are
  the same as the ones created by in the aggregate 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 will first prove 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 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 was 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, and all three
  can be performed independently from each other.

*}

subsection {* Regularization and Injection statements *}

text {*

  The function that gives the statement of the regularized theorem
  takes the statement of the raw theorem (a term) and the statement
  of the lifted theorem. The intuition behind the procedure 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}

  Existential quantifiers and unique existential quantifiers are defined
  similarily to the universal one.

  The function that gives the statment of the injected theorem
  takes the statement of the regularized theorems and the statement
  of the lifted theorem both as terms.

  \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 similarily to the universal one.

*}

subsection {* Proof of Regularization *}

text {*
  Example of non-regularizable theorem ($0 = 1$).


  Separtion of regularization from injection thanks to the following 2 lemmas:
  \begin{lemma}
  If @{term R2} is an equivalence relation, then:
  \begin{eqnarray}
  @{thm (rhs) ball_reg_eqv_range[no_vars]} & = & @{thm (lhs) ball_reg_eqv_range[no_vars]}\\
  @{thm (rhs) bex_reg_eqv_range[no_vars]} & = & @{thm (lhs) bex_reg_eqv_range[no_vars]}
  \end{eqnarray}
  \end{lemma}

  Other lemmas used in regularization:
  @{thm [display] ball_reg_eqv[no_vars]}
  @{thm [display] bex_reg_eqv[no_vars]}
  @{thm [display] babs_reg_eqv[no_vars]}
  @{thm [display] babs_simp[no_vars]}

  @{thm [display] ball_reg_right[no_vars]}
  @{thm [display] bex_reg_left[no_vars]}
  @{thm [display] bex1_bexeq_reg[no_vars]}

*}

subsection {* Injection *}

text {*

  The 2 key lemmas are:

  @{thm [display] apply_rsp[no_vars]}
  @{thm [display] rep_abs_rsp[no_vars]}



*}




subsection {* Cleaning *}

text {* Preservation of quantifiers, abstractions, relations, quotient-constants
  (definitions) and user given constant preservation lemmas *}

section {* Examples *}

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}
*}

(*<*)
end
(*>*)