+
−
(*<*)+
−
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+
−
(*>*)+
−