(*<*)
theory Paper
imports "Quotient" 
        "LaTeXsugar"
begin

notation (latex output)
  fun_rel ("_ ===> _" [51, 51] 50)

(*>*)

section {* Introduction *}

text {* 
  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

  @{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
  The problem is that one 
  


*}

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
    respectfullness and preservation to cope with quotient
    composition.

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

  \item We regularize more thanks to new lemmas. (inductions 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 {*
  Defintion of quotient,

  Equivalence,

  Relation map and function map
*}

section {* Constants *}

text {*
  Rep and Abs, Rsp and Prs
*}

section {* Lifting Theorems *}

text {* TBD *}

text {* Why providing a statement to prove is necessary is some cases *}

subsection {* Regularization *}

text {*
Transformation of the theorem statement:
\begin{itemize}
\item Quantifiers and abstractions involving raw types replaced by bounded ones.
\item Equalities involving raw types replaced by bounded ones.
\end{itemize}

The procedure.

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

New regularization 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}

*}

subsection {* Injection *}

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 (and related work from there), John
    Harrison's one.

  \item Manually defined quotients in Isabelle/HOL Library (Larry's
    quotients, Markus's Quotient\_Type, Dixon's FSet, \ldots)

  \item Oscar Slotosch defines quotient-type automatically but no
    lifting.

  \item PER. And how to avoid it.

  \item Necessity of Hilbert Choice op.

  \item Setoids in Coq

  \end{itemize}
*}

(*<*)
end
(*>*)