diff -r d769c24094cf -r 10148a447359 Quotient-Paper/Paper.thy --- 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 \ 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 "\\<^isub>q"}, and an equivalence relation, say @{text R}, defined over a raw type, say @{text "\"}. 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 "\s"} + indicate the arity of the new type and the type-variables of @{text "\"} can only + be contained in @{text "\s"}. Two concrete examples are @@ -527,7 +524,7 @@ (for the proof see \cite{Homeier05}). \begin{proposition} - @{term "Quotient R Abs_\\<^isub>q Rep_\\<^isub>q"}. + \begin{isa}@{term "Quotient R Abs_\\<^isub>q Rep_\\<^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 "\s + In the last two clauses are subtle. We rely in them on the fact that the type @{text "\s \\<^isub>q"} is the quotient of the raw type @{text "\s \"} (for example @{text "int"} and @{text "nat \ nat"}, or @{text "\ fset"} and @{text "\ - 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 "\s \"} must be among the @{text "\s"}. The @{text "\s'"} are given by the substitutions for the @{text "\s"} when matching @{text "\s \"} against - @{text "\s \"}. The + @{text "\s \"}. This calculation determines what are the types in place + of the type variables @{text "\s"} in the instance of + quotient type @{text "\s \\<^isub>q"}---namely @{text "\s"}, and the corresponding + types in place of the @{text "\s"} in the raw type @{text "\s \"}---namely @{text "\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 "\ \ \ list \ \ list"}) we have \begin{isabelle}\ \ \ \ \ %%% - @{text "(Rep ---> map_list Rep ---> map_list Abs) cons = cons"} + @{text "(Rep \ map_list Rep \ 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 \} is instantiated with @{text "nat \ 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 (\x\<^sup>\. t, \x\<^sup>\. s)"} $\dn$ $\begin{cases} @{text "\x\<^sup>\. REG (t, s)"} \quad\mbox{provided @{text "\ = \"}}\\ - @{text "\x\<^sup>\ \ Respects (REL (\, \)). REG (t, s)"} + @{text "\x\<^sup>\ \ Resp (REL (\, \)). REG (t, s)"} \end{cases}$\smallskip\\ - \\ - \multicolumn{1}{@ {}l}{universal quantifiers:}\\ + \multicolumn{1}{@ {}l@ {}}{universal quantifiers:}\\ @{text "REG (\x\<^sup>\. t, \x\<^sup>\. s)"} $\dn$ $\begin{cases} @{text "\x\<^sup>\. REG (t, s)"} \quad\mbox{provided @{text "\ = \"}}\\ - @{text "\x\<^sup>\ \ Respects (REL (\, \)). REG (t, s)"} + @{text "\x\<^sup>\ \ Resp (REL (\, \)). 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>\\\\bool\<^esup>, =\<^bsup>\\\\bool\<^esup>)"} $\dn$ @{text "REL (\, \)"}\\\smallskip\\ - \multicolumn{1}{@ {}l}{applications, variables and constants:}\\ + @{text "REG (=\<^bsup>\\\\bool\<^esup>, =\<^bsup>\\\\bool\<^esup>)"} $\dn$ @{text "REL (\, \)"}\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 \ reg_thm"}, we always + In the first phase, establishing @{text "raw_thm \ 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 "(\x. R x \ (P x \ Q x)) \ (\x. P x \ \x \ R. Q x)"} - \end{isabelle} + + %In this case we have + %rules of the form + % + % \begin{isabelle}\ \ \ \ \ %%% + %@{text "(\x. R x \ (P x \ Q x)) \ (\x. P x \ \x \ 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 "\x \ Respects R. P x = \x. P x"} - \end{isabelle} + %\begin{isabelle}\ \ \ \ \ %%% + %@{text "\x \ Resp R. P x = \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 \ inj_thm"}, starts with an equality + The second phase, establishing @{text "reg_thm \ 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 "\"}-expand and @{text "\"}-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 "\"}-expand and @{text "\"}-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 \ R x (Rep (Abs y))"} - \end{isabelle} + %\begin{isabelle}\ \ \ \ \ %%% + % @{term "R x y \ 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 \ R\<^isub>2) f g \ R\<^isub>1 x y \ R\<^isub>2 (f x) (g y)"} - \end{isabelle} - \end{itemize} + %\begin{isabelle}\ \ \ \ \ %%% + % @{text "(R\<^isub>1 \ R\<^isub>2) f g \ R\<^isub>1 x y \ 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 \ quot_thm"} can be + establishing in the third phase the equivalence @{text "inj_thm \ 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