nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:d769c24094cf
+:10148a447359
 section {* Introduction *}
 text {*
 \noindent
-One might think they have been studied to death, but in the context of
+One might think quotients have been studied to death, but in the context of
-theorem provers many questions concerning quotients are far from settled. In
+theorem provers many questions concerning them are far from settled. In
-this paper we address the question how a convenient reasoning infrastructure
+this paper we address the question of how to establish a convenient reasoning
-for quotient constructions can be established in Isabelle/HOL, a popular
+infrastructure
-generic theorem prover. Higher-Order Logic (HOL) consists
+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
 the equivalence relation
 according to the type of the raw constant and the type
 of the quotient constant. This means we also have to extend the notions
 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
+In addition we are able to clearly specify what is involved
-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 the lifting process (this was only hinted at in \cite{Homeier05} and
-implemented as a ``rough recipe'' in ML-code).
+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
-%The paper is organised as follows: Section \ref{sec:prelims} presents briefly
+on the quotient level. Space constraints, unfortunately, allow us to only
-%some necessary preliminaries; Section \ref{sec:type} describes the definitions
+sketch this part of our work in Section 5 and we defer the reader to a longer
-%of quotient types and shows how definitions of constants can be made over
+version for the details. However, we will give in Section 3 and 4 all
-%quotient types. Section \ref{sec:resp} introduces the notions of respectfulness
+definitions that specify the input and output data of our three-step
-%and preservation; Section \ref{sec:lift} describes the lifting of theorems;
+lifting procedure. Section 6 gives an example how our quotient package
-%Section \ref{sec:examples} presents some examples
+works in practise.
-%and Section \ref{sec:conc} concludes and compares our results to existing
-%work.
 *}
 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
 recorded in Church-style fashion (that means, we can always infer the type of
 a term and its subterms without any additional information). The grammars
 \noindent
 As a result, Homeier is able to build an automatic prover that can nearly
 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?
 \begin{definition}%%[Composition of Relations]
 *}
 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
 relation must be @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of
 the quotient type declaration is therefore
 \begin{isabelle}\ \ \ \ \ %%%
 \isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}\hfill\numbered{typedecl}
 \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
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 respectively.  Given that @{text "R"} is an equivalence relation, the
 following property holds  for every quotient type
 (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
 involving the quotient type. These definitions need to be given in terms of concepts
 of the raw type (remember this is the only way how to extend HOL
 @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} $\dn$ @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s))) \<circ> Rep_\<kappa>\<^isub>q"}
 \end{tabular}\hfill\numbered{ABSREP}
 \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:
 %
 \begin{center}
 \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 *}
 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
 two restrictions in form of proof obligations that arise during the
 lifting. The reason is that even if definitions for all raw constants
 \noindent
 where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}.
 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]}
 %Given two quotients, one of which quotients a container, and the
 %other quotients the type in the container, we can write the
 %%% lifting theorems. But there is no clarification about the
 %%% correctness. A reader would also be interested in seeing some
 %%% 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
 (Definition \ref{def:respects} states what respects means). The purpose of injection is to add @{term Rep}
 and @{term Abs} of appropriate types in front of constants and variables
 equivalence classes are not equal. In order to obtain @{text "0 \<noteq> 1"}, a
 more general statement stipulating that the equivalence classes are not
 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
 @{text "quot_thm"}. Then we define the statement of the injected theorem, based
 on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps,
 @{text "raw_thm"} and @{text "quot_thm"} as input and returns
 @{text "reg_thm"}. The idea
 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
+equivalence relations. It is defined by simultaneous recursion on
-the structure of  @{text "raw_thm"} and @{text "quot_thm"} as follows:
+the structure of  the terms of @{text "raw_thm"} and @{text "quot_thm"} as follows:
+%
 \begin{center}
-\begin{tabular}{l}
+\begin{tabular}{@ {}l@ {}}
-\multicolumn{1}{@ {}l}{abstractions:}\smallskip\\
+\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\\
+@{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:}\\
+\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"}\\
 \end{tabular}
 \end{center}
 %%% You should clarify under which circumstances the implication is
 %%% being proved here.
 %%% 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
+for instance, a quantifier by a bounded quantifier. To decompose them, we have
-rules of the form
+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)"}
+%In this case we have
-\end{isabelle}
+%rules of the form
+%
-\noindent
+% \begin{isabelle}\ \ \ \ \ %%%
-They decompose a bounded quantifier on the right-hand side. We can decompose a
+%@{text "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}
-bounded quantifier anywhere if R is an equivalence relation or
+%\end{isabelle}
-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
-\begin{isabelle}\ \ \ \ \ %%%
+%bounded quantifier anywhere if R is an equivalence relation or
-@{text "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}
+%if it is a relation over function types with the range being an equivalence
-\end{isabelle}
+%relation. If @{text R} is an equivalence relation we can prove that
-\noindent
+%\begin{isabelle}\ \ \ \ \ %%%
-If @{term R\<^isub>2} is an equivalence relation, we can prove that for any predicate @{term P}
+%@{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}
 %%% FIXME Reviewer 1 claims the theorem is obviously false so maybe we
 %%% should include a proof sketch?
-\begin{isabelle}\ \ \ \ \ %%%
+%\begin{isabelle}\ \ \ \ \ %%%
-@{thm (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
+%@{thm (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
-\end{isabelle}
+%\end{isabelle}
-\noindent
+%\noindent
-The last theorem is new in comparison with Homeier's package. There the
+%The last theorem is new in comparison with Homeier's package. There the
-injection procedure would be used to prove such goals and
+%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,
+%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
+%because this allows us to completely separate the first and the second
-proof step into two independent ``units''.
+%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}
+%\begin{itemize}
-\item For two constants an appropriate respectfulness theorem is applied.
+%\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 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 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
+%\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
+%  @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"} holds. If yes then we
-can apply the theorem:
+%  can apply the theorem:
-\begin{isabelle}\ \ \ \ \ %%%
+%\begin{isabelle}\ \ \ \ \ %%%
-@{term "R x y \<longrightarrow> R x (Rep (Abs y))"}
+%  @{term "R x y \<longrightarrow> R x (Rep (Abs y))"}
-\end{isabelle}
+%\end{isabelle}
-Otherwise we introduce an appropriate relation between the subterms
+%  Otherwise we introduce an appropriate relation between the subterms
-and continue with two subgoals using the lemma:
+%  and continue with two subgoals using the lemma:
-\begin{isabelle}\ \ \ \ \ %%%
+%\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)"}
+%  @{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{isabelle}
-\end{itemize}
+%\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
+definitions. This step also requires that the definitions of all lifted constants
-are used to fold the @{term Rep} with the raw constants. Next for
+are used to fold the @{term Rep} with the raw constants. We will give more details
-all abstractions and quantifiers the lambda and
+about our lifting procedure in a longer version of this paper.
-quantifier preservation theorems are used to replace the
-variables that include raw types with respects by quantifiers
+%Next for
-over variables that include quotient types. We show here only
+%all abstractions and quantifiers the lambda and
-the lambda preservation theorem. Given
+%quantifier preservation theorems are used to replace the
-@{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:
+%variables that include raw types with respects by quantifiers
+%over variables that include quotient types. We show here only
-\begin{isabelle}\ \ \ \ \ %%%
+%the lambda preservation theorem. Given
-@{thm (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
+%@{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:
-\end{isabelle}
+%\begin{isabelle}\ \ \ \ \ %%%
-\noindent
+%@{thm (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
-Next, relations over lifted types can be rewritten to equalities
+%\end{isabelle}
-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
-\begin{isabelle}\ \ \ \ \ %%%
+%over lifted type. Rewriting is performed with the following theorem,
-@{thm (concl) Quotient_rel_rep[no_vars]}
+%which has been shown by Homeier~\cite{Homeier05}:
-\end{isabelle}
+%\begin{isabelle}\ \ \ \ \ %%%
-\noindent
+%@{thm (concl) Quotient_rel_rep[no_vars]}
-Finally, we rewrite with the preservation theorems. This will result
+%\end{isabelle}
-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} *}
 text {*
 %%% FIXME Reviewer 1 would like an example of regularized and injected
 %%% 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.
 A user of our quotient package first needs to define a relation on
 section {* Conclusion and Related Work\label{sec:conc}*}
 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
 heavily used in the new version of Nominal Isabelle, which provides a
 convenient reasoning infrastructure for programming language calculi

changeset 2445	10148a447359
parent 2444	d769c24094cf
child 2455	0bc1db726f81