added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
(*<*)+ −
theory Paper+ −
imports "Quotient" + −
"LaTeXsugar"+ −
begin+ −
+ −
notation (latex output)+ −
fun_rel ("_ ===> _" [51, 51] 50)+ −
+ −
(*>*)+ −
+ −
section {* Introduction *}+ −
+ −
text {* TBD *}+ −
+ −
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+ −
(*>*)+ −