nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:c474186439bd
+:f5b6f9d8a882
 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_map ("_ \<^raw:\mbox{\tt{---\textgreater}}> _" 51) and
-fun_rel (infix "\<Longrightarrow>" 51) and
+fun_rel ("_ \<^raw:\mbox{\tt{===\textgreater}}> _" 51) and
 list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
 fempty ("\<emptyset>") and
 funion ("_ \<union> _") and
 finsert ("{_} \<union> _") and
 Cons ("_::_") and
 This constructions yields the new type @{typ int} and definitions for @{text
 "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of
 natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations
 such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in
 terms of operations on pairs of natural numbers (namely @{text
-"add\<^bsub>nat\<times>nat\<^esub> (n\<^isub>1, m\<^isub>1) (n\<^isub>2,
+"add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2,
 m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}).
 Similarly one can construct the type of finite sets, written @{term "\<alpha> fset"},
 by quotienting the type @{text "\<alpha> list"} according to the equivalence relation
-@{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}
+@{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}
 \noindent
-which states that two lists are equivalent if every element in one list is also
+which states that two lists are equivalent if every element in one list is
-member in the other (@{text "\<in>"} stands here for membership in lists). The
+also member in the other. The empty finite set, written @{term "{||}"}, can
-empty finite set, written @{term "{||}"}, can then be defined as the
+then be defined as the empty list and the union of two finite sets, written
-empty list and the union of two finite sets, written @{text "\<union>"}, as list append.
+@{text "\<union>"}, as list append.
 An area where quotients are ubiquitous is reasoning about programming language
 calculi. A simple example is the lambda-calculus, whose ``raw'' terms are defined as
 @{text [display, indent=10] "t ::= x | t t | \<lambda>x.t"}
 \draw (-2.0,-0.195)  -- (0.7,-0.195);
 \draw ( 0.7, 0.23) node {\begin{tabular}{@ {}c@ {}}equiv-\\[-1mm]clas.\end{tabular}};
 \draw (-2.45, 0.35) node {\begin{tabular}{@ {}c@ {}}new\\[-1mm]type\end{tabular}};
 \draw (1.8, 0.35) node[right=-0.1mm]
-{\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};
+{\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw elements)\end{tabular}};
 \draw (0.9, -0.55) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
 \draw[->, very thick] (-1.8, 0.36) -- (-0.1,0.36);
 \draw[<-, very thick] (-1.8, 0.16) -- (-0.1,0.16);
 \draw (-0.95, 0.26) node[above=0.4mm] {@{text Rep}};
 \end{center}
 \noindent
 The starting point is an existing type over which an equivalence relation
 given by the user is defined. With this input the package introduces a new
-type, which comes with two associated abstraction and representation
+type that comes with associated \emph{abstraction} and \emph{representation}
 functions, written @{text Abs} and @{text Rep}. These functions relate
-elements in the existing and new type, and can be uniquely identified by
+elements in the existing type to ones in the new type and vice versa; they
-their type (which however we often omit for better readability). They
+can be uniquely identified by their type. For example for the integer
-represent an isomorphism between the non-empty subset and elements in the
+quotient construction the types of @{text Abs} and @{text Rep} are
-new type. They are necessary for making definitions involving the new type. For
-example @{text "0"} and @{text "1"} of type @{typ int} can be defined as
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+@{text "Abs::nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep::int \<Rightarrow> nat \<times> nat"}
+\end{isabelle}
+\noindent
+However we often leave this typing information implicit for better
+readability. Every abstraction and representation function represents an
+isomorphism between the non-empty subset and elements in the new type. They
+are necessary for making definitions involving the new type. For example
+@{text "0"} and @{text "1"} of type @{typ int} can be defined as
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 @{text "0 \<equiv> Abs (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs (1, 0)"}
 \end{isabelle}
 \noindent
-Slightly more complicated is the definition of @{text "add"} which has type
+Slightly more complicated is the definition of @{text "add"} having type
 @{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition is as follows
-@{text [display, indent=10] "add n m \<equiv> Abs (add\<^bsub>nat\<times>nat\<^esub> (Rep n) (Rep m))"}
+@{text [display, indent=10] "add n m \<equiv> Abs (add_pair (Rep n) (Rep m))"}
 \noindent
-where we have to take first the representation of @{text n} and @{text m},
+where we take the representation of the arguments @{text n} and @{text m},
-add them according to @{text "add\<^bsub>nat\<times>nat\<^esub>"} and then take the
+add them according to @{text "add_pair"} and then take the
 abstraction of the result.  This is all straightforward and the existing
 quotient packages can deal with such definitions. But what is surprising
 that none of them can deal with slightly more complicated definitions involving
 \emph{compositions} of quotients. Such compositions are needed for example
-in case of finite sets.  For example over lists one can define an operator
+in case of quotienting lists and the operator that flattens lists of lists, defined
-that flattens lists of lists as follows
+as follows
 @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]}
 \noindent
 We expect that the corresponding operator on finite sets, written @{term "fconcat"},
 @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
 \noindent
 The quotient package should provide us with a definition for @{text "\<Union>"} in
-terms of @{text flat}, @{text Rep} and @{text Abs}. The problem is that it
+terms of @{text flat}, @{text Rep} and @{text Abs} (the latter two having
-is not enough to just take the representation of the argument and then
+the type @{text "\<alpha> fset \<Rightarrow> \<alpha> list"} and @{text "\<alpha> list \<Rightarrow> \<alpha> fset"},
-take the abstraction of the result, because in that case we obtain an operator
+respectively). The problem is that the method is used in the existing quotient
-with type @{text "(\<alpha> list) fset \<Rightarrow> \<alpha> fset"}, not the expected
+packages of just taking the representation of the arguments and then take
-@{text "(\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}. It turns out that we need
+the abstraction of the result is \emph{not} enough. The reason is that case in case
-to build aggregate representation and abstraction functions, which in
+of @{text "\<Union>"} we obtain the incorrect definition
-case of @{term "fconcat"} produce the following definition
+@{text [display, indent=10] "\<Union> S \<equiv> Abs (flat (Rep S))"}
-@{text [display, indent=10] "\<Union> S \<equiv> Abs (concat ((map Rep \<circ> Rep) S))"}
+\noindent
+where the right-hand side is not even typable! This problem can be remedied in the
+existing quotient packages by introducing an intermediate step and reasoning
+about faltening of lists of finite sets. However, this remedy is rather
+cumbersome and inelegant in light of our work, which can deal with such
+definitions directly. The solution is that we need to build aggregate
+representation and abstraction functions, which in case of @{text "\<Union>"}
+generate the following definition
+@{text [display, indent=10] "\<Union> S \<equiv> Abs (flat ((map Rep \<circ> Rep) S))"}
 \noindent
 where @{term map} is the usual mapping function for lists. In this paper we
-will present a formal definition for our aggregate abstraction and
+will present a formal definition of our aggregate abstraction and
 representation functions (this definition was omitted in \cite{Homeier05}).
-They generate definitions like the one above for @{text add} and @{text "\<Union>"}
+They generate definitions, like the one above for @{text "\<Union>"},
 according to the type of the ``raw'' constant and the type
-of the quotient constant.
+of the quotient constant. This means we also have to extend the notions
+of \emph{respectfulness} and \emph{preservation} from Homeier
+\cite{Homeier05}.
-*}
+We will also address the criticism by Paulson \cite{Paulson06} cited at the
-subsection {* Contributions *}
+beginning of this section about having to collect theorems that are lifted from the raw
+level to the quotient level. Our quotient package is modular so that it
-text {*
+allows to lift single theorems separately. This has the advantage for the
-We present the detailed lifting procedure, which was not shown before.
+user to develop a formal theory interactively an a natural progression. A
+pleasing result of the modularity is also that we are able to clearly
-The quotient package presented in this paper has the following
+specify what needs to be done in the lifting process (this was only hinted at in
-advantages over existing packages:
+\cite{Homeier05} and implemented as a ``rough recipe'' in ML-code).
-\begin{itemize}
+The paper is organised as follows \ldots
-\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.
+section {* Preliminaries and General Quotient\label{sec:prelims} *}
-\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 {* General Quotient *}
 text {*
 In this section we present the definitions of a quotient that follow
 @{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber
 \end{eqnarray}
 *}
-section {* Constants *}
+section {* Lifting of Definitions *}
 (* Say more about containers? *)
 text {*
 \end{itemize}
 *}
 section {* Conclusion *}
+text {*
+The package is part of the standard distribution of Isabelle.
+*}
+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}
+*}
 (*<*)
 end
 (*>*)

changeset 2224	f5b6f9d8a882
parent 2223	c474186439bd
child 2225	cbffed7d81bd