(* How to change the notation for \<lbrakk> \<rbrakk> meta-level implications? *)+ −
+ −
(*<*)+ −
theory Paper+ −
imports "Quotient"+ −
"LaTeXsugar"+ −
"../Nominal/FSet"+ −
begin+ −
+ −
print_syntax+ −
+ −
notation (latex output)+ −
rel_conj ("_ OOO _" [53, 53] 52)+ −
and+ −
"op -->" (infix "\<rightarrow>" 100)+ −
and+ −
"==>" (infix "\<Rightarrow>" 100)+ −
and+ −
fun_map (infix "\<longrightarrow>" 51)+ −
and+ −
fun_rel (infix "\<Longrightarrow>" 51)+ −
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 {* + −
\begin{flushright}+ −
{\em ``Not using a [quotient] package has its advantages: we do not have to\\ + −
collect all the theorems we shall ever want into one giant list;''}\\+ −
Paulson \cite{Paulson06}+ −
\end{flushright}\smallskip+ −
+ −
\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, Quotients and maps+ −
can be defined 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) \<longrightarrow> 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) \<longrightarrow> 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. Adding composition in last two cases is necessary+ −
for compositional quotients. We ilustrate the different behaviour of the+ −
definition by showing the derived definition of @{term fconcat}:+ −
+ −
@{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. To automatically+ −
lift a theorem that talks about a raw constant, to a theorem about+ −
the quotient type a respectfulness theorem is required.+ −
+ −
A respectfulness condition for a constant 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 after unfolding @{term "op \<Longrightarrow>"} is equivalent to:+ −
+ −
@{thm [display] append_rsp_unfolded[no_vars]}+ −
+ −
An aggregate relation is defined in terms of relation composition,+ −
so we define it first:+ −
+ −
\begin{definition}[Composition of Relations]+ −
@{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate+ −
composition @{thm pred_compI[no_vars]}+ −
\end{definition}+ −
+ −
The aggregate relation for an aggregate raw type and quotient type+ −
is defined as:+ −
+ −
\begin{itemize}+ −
\item @{text "REL(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "op ="}+ −
\item @{text "REL(\<sigma>, \<sigma>)"} = @{text "op ="}+ −
\item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"} = @{text "(rel \<kappa>) (REL(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REL(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}+ −
\item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"} = @{text "(rel \<kappa>\<^isub>1) (REL(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REL(\<rho>\<^isub>p,\<nu>\<^isub>p) OOO Eqv_\<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}+ −
+ −
Again, the last case is novel, so lets look at the example of+ −
respectfullness for @{term concat}. The statement according to+ −
the definition 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 as defined above+ −
and the abstraction and relation functions are the ones of the sub+ −
quotients composed with the usual function composition.+ −
The @{term "Rep"} and @{term "Abs"} functions that we obtain agree+ −
with the definition of aggregate Abs/Rep 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 provide 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 were 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, as all three+ −
can be performed independently from each other.+ −
+ −
*}+ −
+ −
subsection {* Regularization and Injection statements *}+ −
+ −
text {*+ −
+ −
We first define the function @{text REG}, which takes the statements+ −
of the raw theorem and the lifted theorem (both as terms) and+ −
returns the statement of the regularized version. The intuition+ −
behind this function 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}+ −
+ −
In the above definition we ommited the cases for existential quantifiers+ −
and unique existential quantifiers, as they are very similar to the cases+ −
for the universal quantifier.+ −
+ −
Next we define the function @{text INJ} which takes the statement of+ −
the regularized theorems and the statement of the lifted theorem both as+ −
terms and returns the statment of the injected theorem:+ −
+ −
\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 procedure *}+ −
+ −
(* In the below the type-guiding 'QuotTrue' assumption is removed; since we+ −
present in a paper a version with typed-variables it is not necessary *)+ −
+ −
text {*+ −
+ −
With the above definitions of @{text "REG"} and @{text "INJ"} we can show+ −
how the proof is performed. The first step is always the application of+ −
of the following lemma:+ −
+ −
@{term "[|A; A --> B; B = C; C = D|] ==> D"}+ −
+ −
With @{text A} instantiated to the original raw theorem, + −
@{text B} instantiated to @{text "REG(A)"},+ −
@{text C} instantiated to @{text "INJ(REG(A))"},+ −
and @{text D} instantiated to the statement of the lifted theorem.+ −
The first assumption can be immediately discharged using the original+ −
theorem and the three left subgoals are exactly the subgoals of regularization,+ −
injection and cleaning. The three can be proved independently by the+ −
framework and in case there are non-solved subgoals they can be left+ −
to the user.+ −
+ −
The injection and cleaning subgoals are always solved if the appropriate+ −
respectfulness and preservation theorems are given. It is not the case+ −
with regularization; sometimes a theorem given by the user does not+ −
imply a regularized version and a stronger one needs to be proved. This+ −
is outside of the scope of the quotient package, so the user is then left+ −
with such obligations. As an example lets see the simplest possible+ −
non-liftable theorem for integers: When we want to prove @{term "0 \<noteq> 1"}+ −
on integers the fact that @{term "\<not> (0, 0) = (1, 0)"} is not enough. It+ −
only shows that particular items in the equivalence classes are not equal,+ −
a more general statement saying that the classes are not equal is necessary.+ −
*}+ −
+ −
subsection {* Proving Regularization *}+ −
+ −
text {*+ −
+ −
Isabelle provides a set of \emph{mono} rules, that are used to split implications+ −
of similar statements into simpler implication subgoals. These are enchanced+ −
with special quotient theorem in the regularization goal. Below we only show+ −
the versions for the universal quantifier. For the existential quantifier+ −
and abstraction they are analoguous with some symmetry.+ −
+ −
First, bounded universal quantifiers can be removed on the right:+ −
+ −
@{thm [display] ball_reg_right[no_vars]}+ −
+ −
They can be removed anywhere if the relation is an equivalence relation:+ −
+ −
@{thm [display] ball_reg_eqv[no_vars]}+ −
+ −
And finally it can be removed anywhere if @{term R2} is an equivalence relation, then:+ −
\[+ −
@{thm (rhs) ball_reg_eqv_range[no_vars]} = @{thm (lhs) ball_reg_eqv_range[no_vars]}+ −
\]+ −
+ −
The last theorem is new in comparison with Homeier's package; it allows separating+ −
regularization from injection.+ −
+ −
*}+ −
+ −
(*+ −
@{thm (rhs) bex_reg_eqv_range[no_vars]} = @{thm (lhs) bex_reg_eqv_range[no_vars]}+ −
@{thm [display] bex_reg_left[no_vars]}+ −
@{thm [display] bex1_bexeq_reg[no_vars]}+ −
@{thm [display] bex_reg_eqv[no_vars]}+ −
@{thm [display] babs_reg_eqv[no_vars]}+ −
@{thm [display] babs_simp[no_vars]}+ −
*)+ −
+ −
subsection {* Injection *}+ −
+ −
text {*+ −
The injection proof starts with an equality between the regularized theorem+ −
and the injected version. The proof again follows by the structure of the+ −
two term, and is defined for a goal being a relation between the two terms.+ −
+ −
\begin{itemize}+ −
\item For two constants, an appropriate constant respectfullness assumption is used.+ −
\item For two variables, the regularization assumptions state that they are related.+ −
\item For two abstractions, they are eta-expanded and beta-reduced.+ −
\end{itemize}+ −
+ −
Otherwise the two terms are applications. There are two cases: If there is a REP/ABS+ −
in the injected theorem we can use the theorem:+ −
+ −
@{thm [display] rep_abs_rsp[no_vars]}+ −
+ −
and continue the proof.+ −
+ −
Otherwise we introduce an appropriate relation between the subterms and continue with+ −
two subgoals using the lemma:+ −
+ −
@{thm [display] apply_rsp[no_vars]}+ −
+ −
*}+ −
+ −
subsection {* Cleaning *}+ −
+ −
text {*+ −
The @{text REG} and @{text INJ} functions have been defined in such a way+ −
that establishing the goal theorem now consists only on rewriting the+ −
injected theorem with the preservation theorems.+ −
+ −
\begin{itemize}+ −
\item First for lifted constants, their definitions are the preservation rules for+ −
them.+ −
\item For lambda abstractions lambda preservation establishes+ −
the equality between the injected theorem and the goal. This allows both+ −
abstraction and quantification over lifted types.+ −
@{thm [display] lambda_prs[no_vars]}+ −
\item Relations over lifted types are folded with:+ −
@{thm [display] Quotient_rel_rep[no_vars]}+ −
\item User given preservation theorems, that allow using higher level operations+ −
and containers of types being lifted. An example may be+ −
@{thm [display] map_prs(1)[no_vars]}+ −
\end{itemize}+ −
+ −
Preservation of relations and user given constant preservation lemmas *}+ −
+ −
section {* Examples *}+ −
+ −
(* Mention why equivalence *)+ −
+ −
text {*+ −
+ −
A user of our quotient package first needs to define an equivalence relation:+ −
+ −
@{text "fun \<approx> where (x, y) \<approx> (u, v) = (x + v = u + y)"}+ −
+ −
Then the user defines a quotient type:+ −
+ −
@{text "quotient_type int = (nat \<times> nat) / \<approx>"}+ −
+ −
Which leaves a proof obligation that the relation is an equivalence relation,+ −
that can be solved with the automatic tactic with two definitions.+ −
+ −
The user can then specify the constants on the quotient type:+ −
+ −
@{text "quotient_definition 0 \<Colon> int is (0\<Colon>nat, 0\<Colon>nat)"}+ −
@{text "fun plus_raw where plus_raw (x, y) (u, v) = (x + u, y + v)"}+ −
@{text "quotient_definition (op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int) is plus_raw"}+ −
+ −
Lets first take a simple theorem about addition on the raw level:+ −
+ −
@{text "lemma plus_zero_raw: plus_raw (0, 0) i \<approx> i"}+ −
+ −
When the user tries to lift a theorem about integer addition, the respectfulness+ −
proof obligation is left, so let us prove it first:+ −
+ −
@{text "lemma (op \<approx> \<Longrightarrow> op \<approx> \<Longrightarrow> op \<approx>) plus_raw plus_raw"}+ −
+ −
Can be proved automatically by the system just by unfolding the definition+ −
of @{term "op \<Longrightarrow>"}.+ −
+ −
Now the user can either prove a lifted lemma explicitely:+ −
+ −
@{text "lemma 0 + i = i by lifting plus_zero_raw"}+ −
+ −
Or in this simple case use the automated translation mechanism:+ −
+ −
@{text "thm plus_zero_raw[quot_lifted]"}+ −
+ −
obtaining the same result.+ −
*}+ −
+ −
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}+ −
*}+ −
+ −
section {* Conclusion *}+ −
+ −
(*<*)+ −
end+ −
(*>*)+ −