--- a/Quotient-Paper/Paper.thy Fri Aug 27 19:06:30 2010 +0800
+++ b/Quotient-Paper/Paper.thy Fri Aug 27 23:26:00 2010 +0800
@@ -64,16 +64,17 @@
text {*
\noindent
- One might think they have been studied to death, but in the context of
- theorem provers many questions concerning quotients are far from settled. In
- this paper we address the question how a convenient reasoning infrastructure
- for quotient constructions can be established in Isabelle/HOL, a popular
- generic theorem prover. Higher-Order Logic (HOL) consists
+ One might think quotients have been studied to death, but in the context of
+ theorem provers many questions concerning them are far from settled. In
+ this paper we address the question of how to establish a convenient reasoning
+ infrastructure
+ for quotient constructions in the Isabelle/HOL,
+ theorem prover. Higher-Order Logic (HOL) 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 how
+ identifying non-empty subsets in existing types. Previous work has shown how
to use both mechanisms for dealing with quotient constructions in HOL (see
\cite{Homeier05,Paulson06}). For example the integers in Isabelle/HOL are
constructed by a quotient construction over the type @{typ "nat \<times> nat"} and
@@ -275,32 +276,24 @@
of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}
from Homeier \cite{Homeier05}.
- In addition we are able to address the criticism by Paulson \cite{Paulson06} cited
- at the beginning of this section about having to collect theorems that are
- lifted from the raw level to the quotient level into one giant list. Homeier's and
- also our quotient package are modular so that they allow lifting
- theorems separately. This has the advantage for the user of being able to develop a
- formal theory interactively as a natural progression. A pleasing side-result of
- the modularity is that we are able to clearly specify what is involved
+ In addition we are able to clearly specify what is involved
in the lifting process (this was only hinted at in \cite{Homeier05} and
- implemented as a ``rough recipe'' in ML-code).
-
-
- %The paper is organised as follows: Section \ref{sec:prelims} presents briefly
- %some necessary preliminaries; Section \ref{sec:type} describes the definitions
- %of quotient types and shows how definitions of constants can be made over
- %quotient types. Section \ref{sec:resp} introduces the notions of respectfulness
- %and preservation; Section \ref{sec:lift} describes the lifting of theorems;
- %Section \ref{sec:examples} presents some examples
- %and Section \ref{sec:conc} concludes and compares our results to existing
- %work.
+ implemented as a ``rough recipe'' in ML-code). A pleasing side-result
+ is that our procedure for lifting theorems is completely deterministic
+ following the structure of the theorem being lifted and the theorem
+ on the quotient level. Space constraints, unfortunately, allow us to only
+ sketch this part of our work in Section 5 and we defer the reader to a longer
+ version for the details. However, we will give in Section 3 and 4 all
+ definitions that specify the input and output data of our three-step
+ lifting procedure. Section 6 gives an example how our quotient package
+ works in practise.
*}
section {* Preliminaries and General\\ Quotients\label{sec:prelims} *}
text {*
\noindent
- We give in this section a crude overview of HOL and describe the main
+ We will give in this section a crude overview of HOL and describe the main
definitions given by Homeier for quotients \cite{Homeier05}.
At its core, HOL is based on a simply-typed term language, where types are
@@ -428,7 +421,8 @@
always discharge a proof obligation involving @{text "Quot"}. Our quotient
package makes heavy
use of this part of Homeier's work including an extension
- for dealing with compositions of equivalence relations defined as follows:
+ for dealing with \emph{conjugations} of equivalence relations\footnote{That are
+ symmetric by definition.} defined as follows:
%%% FIXME Referee 2 claims that composition-of-relations means OO, and this is also
%%% what wikipedia says. Any idea for a different name? Conjugation of Relations?
@@ -463,6 +457,7 @@
section {* Quotient Types and Quotient\\ Definitions\label{sec:type} *}
text {*
+ \noindent
The first step in a quotient construction is to take a name for the new
type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},
defined over a raw type, say @{text "\<sigma>"}. The type of the equivalence
@@ -474,7 +469,9 @@
\end{isabelle}
\noindent
- and a proof that @{text "R"} is indeed an equivalence relation. Two concrete
+ and a proof that @{text "R"} is indeed an equivalence relation. The @{text "\<alpha>s"}
+ indicate the arity of the new type and the type-variables of @{text "\<sigma>"} can only
+ be contained in @{text "\<alpha>s"}. Two concrete
examples are
@@ -527,7 +524,7 @@
(for the proof see \cite{Homeier05}).
\begin{proposition}
- @{term "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.
+ \begin{isa}@{term "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.\end{isa}
\end{proposition}
The next step in a quotient construction is to introduce definitions of new constants
@@ -591,13 +588,17 @@
\end{center}
%
\noindent
- In the last two clauses we rely on the fact that the type @{text "\<alpha>s
+ In the last two clauses are subtle. We rely in them on the fact that the type @{text "\<alpha>s
\<kappa>\<^isub>q"} is the quotient of the raw type @{text "\<rho>s \<kappa>"} (for example
@{text "int"} and @{text "nat \<times> nat"}, or @{text "\<alpha> fset"} and @{text "\<alpha>
- list"}). The quotient construction ensures that the type variables in @{text
+ list"}). This data is given by declarations shown in \eqref{typedecl}.
+ The quotient construction ensures that the type variables in @{text
"\<rho>s \<kappa>"} must be among the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
substitutions for the @{text "\<alpha>s"} when matching @{text "\<sigma>s \<kappa>"} against
- @{text "\<rho>s \<kappa>"}. The
+ @{text "\<rho>s \<kappa>"}. This calculation determines what are the types in place
+ of the type variables @{text "\<alpha>s"} in the instance of
+ quotient type @{text "\<alpha>s \<kappa>\<^isub>q"}---namely @{text "\<tau>s"}, and the corresponding
+ types in place of the @{text "\<alpha>s"} in the raw type @{text "\<rho>s \<kappa>"}---namely @{text "\<sigma>s'"}. The
function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw
type as follows:
%
@@ -716,6 +717,7 @@
section {* Respectfulness and\\ Preservation \label{sec:resp} *}
text {*
+ \noindent
The main point of the quotient package is to automatically ``lift'' theorems
involving constants over the raw type to theorems involving constants over
the quotient type. Before we can describe this lifting process, we need to impose
@@ -853,14 +855,14 @@
In case of @{text cons} (which has type @{text "\<alpha> \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"}) we have
\begin{isabelle}\ \ \ \ \ %%%
- @{text "(Rep ---> map_list Rep ---> map_list Abs) cons = cons"}
+ @{text "(Rep \<singlearr> map_list Rep \<singlearr> map_list Abs) cons = cons"}
\end{isabelle}
\noindent
- under the assumption @{text "Quotient R Abs Rep"}. Interestingly, if we have
+ under the assumption @{text "Quotient R Abs Rep"}. The point is that if we have
an instance of @{text cons} where the type variable @{text \<alpha>} is instantiated
with @{text "nat \<times> nat"} and we also quotient this type to yield integers,
- then we need to show the corresponding preservation property.
+ then we need to show this preservation property.
%%%@ {thm [display, indent=10] insert_preserve2[no_vars]}
@@ -902,10 +904,14 @@
%%% discussions about the generality and limitation of the approach
%%% proposed there
+ \noindent
The main benefit of a quotient package is to lift automatically theorems over raw
types to theorems over quotient types. We will perform this lifting in
three phases, called \emph{regularization},
\emph{injection} and \emph{cleaning} according to procedures in Homeier's ML-code.
+ Space restrictions, unfortunately, prevent us from giving anything but a sketch of these three
+ phases. However, we will precisely define the input and output data of these phases
+ (this was omitted in \cite{Homeier05}).
The purpose of regularization is to change the quantifiers and abstractions
in a ``raw'' theorem to quantifiers over variables that respect their respective relations
@@ -948,7 +954,8 @@
equal is necessary. This kind of failure is beyond the scope where the
quotient package can help: the user has to provide a raw theorem that
can be regularized automatically, or has to provide an explicit proof
- for the first proof step.
+ for the first proof step. Homeier gives more details about this issue
+ in the long version of \cite{Homeier05}.
In the following we will first define the statement of the
regularized theorem based on @{text "raw_thm"} and
@@ -962,28 +969,27 @@
behind this function is that it replaces quantifiers and
abstractions involving raw types by bounded ones, and equalities
involving raw types by appropriate aggregate
- equivalence relations. It is defined by simultaneously recursing on
- the structure of @{text "raw_thm"} and @{text "quot_thm"} as follows:
-
+ equivalence relations. It is defined by simultaneous recursion on
+ the structure of the terms of @{text "raw_thm"} and @{text "quot_thm"} as follows:
+ %
\begin{center}
- \begin{tabular}{l}
- \multicolumn{1}{@ {}l}{abstractions:}\smallskip\\
+ \begin{tabular}{@ {}l@ {}}
+ \multicolumn{1}{@ {}l@ {}}{abstractions:}\smallskip\\
@{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} $\dn$
$\begin{cases}
@{text "\<lambda>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
- @{text "\<lambda>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
+ @{text "\<lambda>x\<^sup>\<sigma> \<in> Resp (REL (\<sigma>, \<tau>)). REG (t, s)"}
\end{cases}$\smallskip\\
- \\
- \multicolumn{1}{@ {}l}{universal quantifiers:}\\
+ \multicolumn{1}{@ {}l@ {}}{universal quantifiers:}\\
@{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} $\dn$
$\begin{cases}
@{text "\<forall>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
- @{text "\<forall>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
+ @{text "\<forall>x\<^sup>\<sigma> \<in> Resp (REL (\<sigma>, \<tau>)). REG (t, s)"}
\end{cases}$\smallskip\\
- \multicolumn{1}{@ {}l}{equality:}\smallskip\\
+ \multicolumn{1}{@ {}l@ {}}{equality:}\smallskip\\
%% REL of two equal types is the equality so we do not need a separate case
- @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} $\dn$ @{text "REL (\<sigma>, \<tau>)"}\\\smallskip\\
- \multicolumn{1}{@ {}l}{applications, variables and constants:}\\
+ @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} $\dn$ @{text "REL (\<sigma>, \<tau>)"}\smallskip\\
+ \multicolumn{1}{@ {}l@ {}}{applications, variables and constants:}\\
@{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} $\dn$ @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
@{text "REG (x\<^isub>1, x\<^isub>2)"} $\dn$ @{text "x\<^isub>1"}\\
@{text "REG (c\<^isub>1, c\<^isub>2)"} $\dn$ @{text "c\<^isub>1"}\\
@@ -1040,98 +1046,105 @@
%%% Cezary: It would be nice to cite Homeiers discussions in the
%%% Quotient Package manual from HOL (the longer paper), do you agree?
- In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always
+ In the first phase, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always
start with an implication. Isabelle provides \emph{mono} rules that can split up
the implications into simpler implicational subgoals. This succeeds for every
monotone connective, except in places where the function @{text REG} replaced,
- for instance, a quantifier by a bounded quantifier. In this case we have
- rules of the form
+ for instance, a quantifier by a bounded quantifier. To decompose them, we have
+ to prove that the relations involved are aggregate equivalence relations.
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}
- \end{isabelle}
+
+ %In this case we have
+ %rules of the form
+ %
+ % \begin{isabelle}\ \ \ \ \ %%%
+ %@{text "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}
+ %\end{isabelle}
- \noindent
- They decompose a bounded quantifier on the right-hand side. We can decompose a
- bounded quantifier anywhere if R is an equivalence relation or
- if it is a relation over function types with the range being an equivalence
- relation. If @{text R} is an equivalence relation we can prove that
+ %\noindent
+ %They decompose a bounded quantifier on the right-hand side. We can decompose a
+ %bounded quantifier anywhere if R is an equivalence relation or
+ %if it is a relation over function types with the range being an equivalence
+ %relation. If @{text R} is an equivalence relation we can prove that
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}
- \end{isabelle}
+ %\begin{isabelle}\ \ \ \ \ %%%
+ %@{text "\<forall>x \<in> Resp R. P x = \<forall>x. P x"}
+ %\end{isabelle}
- \noindent
- If @{term R\<^isub>2} is an equivalence relation, we can prove that for any predicate @{term P}
+ %\noindent
+ %If @{term R\<^isub>2} is an equivalence relation, we can prove that for any predicate @{term P}
%%% FIXME Reviewer 1 claims the theorem is obviously false so maybe we
%%% should include a proof sketch?
- \begin{isabelle}\ \ \ \ \ %%%
- @{thm (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
- \end{isabelle}
+ %\begin{isabelle}\ \ \ \ \ %%%
+ %@{thm (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
+ %\end{isabelle}
- \noindent
- The last theorem is new in comparison with Homeier's package. There the
- injection procedure would be used to prove such goals and
- the assumption about the equivalence relation would be used. We use the above theorem directly,
- because this allows us to completely separate the first and the second
- proof step into two independent ``units''.
+ %\noindent
+ %The last theorem is new in comparison with Homeier's package. There the
+ %injection procedure would be used to prove such goals and
+ %the assumption about the equivalence relation would be used. We use the above theorem directly,
+ %because this allows us to completely separate the first and the second
+ %proof step into two independent ``units''.
- The second proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"}, starts with an equality
+ The second phase, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"}, starts with an equality
between the terms of the regularized theorem and the injected theorem.
The proof again follows the structure of the
- two underlying terms and is defined for a goal being a relation between these two terms.
+ two underlying terms taking respectfulness theorems into account.
- \begin{itemize}
- \item For two constants an appropriate respectfulness theorem is applied.
- \item For two variables, we use the assumptions proved in the regularization step.
- \item For two abstractions, we @{text "\<eta>"}-expand and @{text "\<beta>"}-reduce them.
- \item For two applications, we check that the right-hand side is an application of
- @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"} holds. If yes then we
- can apply the theorem:
+ %\begin{itemize}
+ %\item For two constants an appropriate respectfulness theorem is applied.
+ %\item For two variables, we use the assumptions proved in the regularization step.
+ %\item For two abstractions, we @{text "\<eta>"}-expand and @{text "\<beta>"}-reduce them.
+ %\item For two applications, we check that the right-hand side is an application of
+ % @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"} holds. If yes then we
+ % can apply the theorem:
- \begin{isabelle}\ \ \ \ \ %%%
- @{term "R x y \<longrightarrow> R x (Rep (Abs y))"}
- \end{isabelle}
+ %\begin{isabelle}\ \ \ \ \ %%%
+ % @{term "R x y \<longrightarrow> R x (Rep (Abs y))"}
+ %\end{isabelle}
- Otherwise we introduce an appropriate relation between the subterms
- and continue with two subgoals using the lemma:
+ % Otherwise we introduce an appropriate relation between the subterms
+ % and continue with two subgoals using the lemma:
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "(R\<^isub>1 \<doublearr> R\<^isub>2) f g \<longrightarrow> R\<^isub>1 x y \<longrightarrow> R\<^isub>2 (f x) (g y)"}
- \end{isabelle}
- \end{itemize}
+ %\begin{isabelle}\ \ \ \ \ %%%
+ % @{text "(R\<^isub>1 \<doublearr> R\<^isub>2) f g \<longrightarrow> R\<^isub>1 x y \<longrightarrow> R\<^isub>2 (f x) (g y)"}
+ %\end{isabelle}
+ %\end{itemize}
We defined the theorem @{text "inj_thm"} in such a way that
- establishing the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be
+ establishing in the third phase the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be
achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient
- definitions. First the definitions of all lifted constants
- are used to fold the @{term Rep} with the raw constants. Next for
- all abstractions and quantifiers the lambda and
- quantifier preservation theorems are used to replace the
- variables that include raw types with respects by quantifiers
- over variables that include quotient types. We show here only
- the lambda preservation theorem. Given
- @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}, we have:
+ definitions. This step also requires that the definitions of all lifted constants
+ are used to fold the @{term Rep} with the raw constants. We will give more details
+ about our lifting procedure in a longer version of this paper.
+
+ %Next for
+ %all abstractions and quantifiers the lambda and
+ %quantifier preservation theorems are used to replace the
+ %variables that include raw types with respects by quantifiers
+ %over variables that include quotient types. We show here only
+ %the lambda preservation theorem. Given
+ %@{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}, we have:
- \begin{isabelle}\ \ \ \ \ %%%
- @{thm (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
- \end{isabelle}
+ %\begin{isabelle}\ \ \ \ \ %%%
+ %@{thm (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
+ %\end{isabelle}
- \noindent
- Next, relations over lifted types can be rewritten to equalities
- over lifted type. Rewriting is performed with the following theorem,
- which has been shown by Homeier~\cite{Homeier05}:
+ %\noindent
+ %Next, relations over lifted types can be rewritten to equalities
+ %over lifted type. Rewriting is performed with the following theorem,
+ %which has been shown by Homeier~\cite{Homeier05}:
- \begin{isabelle}\ \ \ \ \ %%%
- @{thm (concl) Quotient_rel_rep[no_vars]}
- \end{isabelle}
+ %\begin{isabelle}\ \ \ \ \ %%%
+ %@{thm (concl) Quotient_rel_rep[no_vars]}
+ %\end{isabelle}
- \noindent
- Finally, we rewrite with the preservation theorems. This will result
- in two equal terms that can be solved by reflexivity.
- *}
+
+ %Finally, we rewrite with the preservation theorems. This will result
+ %in two equal terms that can be solved by reflexivity.
+*}
section {* Examples \label{sec:examples} *}
@@ -1142,6 +1155,7 @@
%%% statements. He asks for the examples twice, but I would still ignore
%%% it due to lack of space...
+ \noindent
In this section we will show a sequence of declarations for defining the
type of integers by quotienting pairs of natural numbers, and
lifting one theorem.
@@ -1229,6 +1243,7 @@
text {*
+ \noindent
The code of the quotient package and the examples described here are already
included in the standard distribution of Isabelle.\footnote{Available from
\href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} The package is