nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:22c6b6144abd
+:8035515bbbc6
 Nominal Isabelle, then manual reasoning is not an option.
 The purpose of a \emph{quotient package} is to ease the lifting of theorems
 and automate the definitions and reasoning as much as possible. In the
 context of HOL, there have been a few quotient packages already
-\cite{harrison-thesis,Slotosch97}. The most notable is the one by Homeier
+\cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier
 \cite{Homeier05} implemented in HOL4.  The fundamental construction these
 quotient packages perform can be illustrated by the following picture:
 \begin{center}
 \mbox{}\hspace{20mm}\begin{tikzpicture}
 \end{tikzpicture}
 \end{center}
 \noindent
-The starting point is an existing type, often referred to as the
+The starting point is an existing type, often referred to as the \emph{raw
-\emph{raw level}, over which an equivalence relation given by the user is
+type}, over which an equivalence relation given by the user is
 defined. With this input the package introduces a new type, to which we
-refer as the \emph{quotient level}. This type comes with an
+refer as the \emph{quotient type}. This type comes with an
 \emph{abstraction} and a \emph{representation} function, written @{text Abs}
-and @{text Rep}. These functions relate elements in the existing type to
+and @{text Rep}.\footnote{Actually they need to be derived from slightly
-ones in the new type and vice versa; they can be uniquely identified by
+more basic functions. We will show the details later. } These functions
-their type. For example for the integer quotient construction the types of
+relate elements in the existing type to ones in the new type and vice versa;
-@{text Abs} and @{text Rep} are
+they can be uniquely identified by their type. For example for the integer
+quotient construction the types of @{text Abs} and @{text Rep} are
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-@{text "Abs::nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep::int \<Rightarrow> nat \<times> nat"}
+@{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, but sometimes write @{text Abs_int} and @{text Rep_int} if the
 @{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"},
-behaves as follows:
+builds the union of finite sets of finite sets:
 @{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
 respectively). The problem is that the method  used in the existing quotient
 packages of just taking the representation of the arguments and then take
 the abstraction of the result is \emph{not} enough. The reason is that case in case
 of @{text "\<Union>"} we obtain the incorrect definition
-@{text [display, indent=10] "\<Union> S \<equiv> Abs (flat (Rep S))"}
+@{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat (Rep_fset 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 flattening 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))"}
+@{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat ((map Rep_fset \<circ> Rep_fset) S))"}
 \noindent
 where @{term map} is the usual mapping function for lists. In this paper we
 will present a formal definition of our aggregate abstraction and
 representation functions (this definition was omitted in \cite{Homeier05}).
 @{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}
+{\it Say more about containers / maping functions }
 *}
 section {* Quotient Types and Lifting of Definitions *}
-(* Say more about containers? *)
+text {*
+The first step in a quotient constructions is to take a name for the new
-text {*
+type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation defined over a
+raw type, say @{text "\<sigma>"}. The equivalence relation for the quotient
+construction, lets say @{text "R"}, must then be of type @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
+bool"}. Given this data, we can automatically declare the quotient type as
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+\isacommand{typedef}~~@{text "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>x. c = R x}"}
+\end{isabelle}
+\noindent
+being the set of equivalence classes of @{text "R"}. The restriction in this declaration
+is that the type variables in the raw type @{text "\<sigma>"} must be included in the
+type variables @{text "\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will provide us
+with abstraction and representation functions having the type
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+@{text "abs_\<kappa>\<^isub>q :: \<sigma> set \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"}\hspace{10mm}@{text "rep_\<kappa>\<^isub>q :: \<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma> set"}
+\end{isabelle}
+\noindent
+relating the new quotient type and raw type. However, as Homeier noted, it is easier
+to work with the following derived definitions
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+@{text "Abs_\<kappa>\<^isub>q x \<equiv> abs_\<kappa>\<^isub>q (R x)"}\hspace{10mm}@{text "Rep_\<kappa>\<^isub>q x \<equiv> \<epsilon> (rep_\<kappa>\<^isub>q x)"}
+\end{isabelle}
+\noindent
+on the expense of having to use Hilbert's choice operator @{text "\<epsilon>"}. With these
+definitions the abstraction and representation functions relate directly the
+quotient and raw types (their type is  @{text "\<sigma> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"},
+respectively). We can show that the property
+@{text [display, indent=10] "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
+\noindent
+holds (for the proof see \cite{Homeier05}).
 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
 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:
 {\it the first argument is the raw type and the second argument the quotient type}
+%
 \begin{center}
-\begin{tabular}{rcl}
+\begin{longtable}{rcl}
-% type variable case says that variables must be equal...therefore subsumed by the equal case below
-%
-%\multicolumn{3}{@ {\hspace{-4mm}}l}{type variables:}\\
-%@{text "ABS (\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} & $\dn$ & @{text "id"}\\
-%@{text "REP (\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} & $\dn$ & @{text "id"}\smallskip\\
 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
 @{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\\
 @{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\smallskip\\
 \multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\
 @{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
 @{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\
 @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\
 @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\
 \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\
-@{text "ABS (\<sigma>s \<kappa>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>2 \<circ> (MAP(\<rho>s \<kappa>\<^isub>1) (ABS (\<sigma>s', \<tau>s')))"}\\
+@{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s')))"}\\
-@{text "REP (\<sigma>s \<kappa>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>\<^isub>1) (REP (\<sigma>s', \<tau>s'))) \<circ> Rep_\<kappa>\<^isub>2"}\\
+@{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}
+\end{longtable}
 \end{center}
+%
 \noindent
-where in the last two clauses we have that the quotient type @{text "\<alpha>s \<kappa>\<^isub>2"} is a quotient of
+where in the last two clauses we have that the quotient type @{text "\<alpha>s \<kappa>\<^isub>q"} is a quotient of
-the raw type @{text "\<rho>s \<kappa>\<^isub>1"} (for example @{text "\<alpha> fset"} and @{text "\<alpha> list"}).
+the raw type @{text "\<rho>s \<kappa>"} (for example @{text "\<alpha> fset"} and @{text "\<alpha> list"}).
 The quotient construction ensures that the type variables in @{text "\<rho>s"}
 must be amongst the @{text "\<alpha>s"}. Now the @{text "\<sigma>s'"} are given by the matchers
 for the @{text "\<alpha>s"}
-when matching  @{text "\<sigma>s \<kappa>\<^isub>2"} against @{text "\<alpha>s \<kappa>\<^isub>2"}; similarly the @{text "\<tau>s'"} are given by the
+when matching  @{text "\<sigma>s \<kappa>\<^isub>q"} against @{text "\<alpha>s \<kappa>\<^isub>q"}; similarly the @{text "\<tau>s'"} are given by the
-same type-variables when matching @{text "\<tau>s \<kappa>\<^isub>1"} against @{text "\<rho>s \<kappa>\<^isub>1"}.
+same type-variables when matching @{text "\<tau>s \<kappa>"} against @{text "\<rho>s \<kappa>"}.
 The function @{text "MAP"} calculates an \emph{aggregate map-function} for a type
 as follows:
 \begin{center}
 \begin{tabular}{rcl}

changeset 2234	8035515bbbc6
parent 2233	22c6b6144abd
child 2235	ad725de6e39b