(*<*)

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)

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 concat.simps(1)}\\

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

  \noindent

  \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

    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}

  @{thm fun_rel_def[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}

*}

section {* Constants *}

text {*

  \begin{itemize}

  \item For equal types or free type variables return identity.

  \item For function types recurse, change the Rep/Abs flag to

     the opposite one for the domain type and compose the

     results with @{term "fun_map"}.

  \item For equal type constructors use the appropriate map function

     applied to the results for the arguments.

  \end{itemize}

*}

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$).

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}

*}

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~\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

(*>*)