(*<*)+
−
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}+
−
+
−
*}+
−
+
−
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 our algorithm uses the+
−
  same kind of maps. Given the raw compound type and the quotient compound+
−
  type the Rep/Abs algorithm does:+
−
+
−
  \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.+
−
+
−
  \item For unequal type constructors, look in the quotients information+
−
    for a quotient type that matches the type constructor, and instantiate+
−
    the raw type+
−
    appropriately getting back an instantiation environment. We apply+
−
    the environment to the arguments and recurse composing it with the+
−
    aggregate map function.+
−
  \end{itemize}+
−
+
−
  The first three points above are identical to the algorithm present in+
−
  in Homeier's HOL implementation, below is the definition of @{term fconcat}+
−
  that shows the last step:+
−
+
−
  @{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.+
−
*}+
−
+
−
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 {* 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+
−
(*>*)+
−