nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:ea0cdb7c6455
+:2668486b684a
 \begin{isabelle}\ \ \ \ \ %%%
 @{text "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + m\<^isub>2 = m\<^isub>1 + n\<^isub>2"}\hfill\numbered{natpairequiv}
 \end{isabelle}
 \noindent
-This constructions yields the new type @{typ int} and definitions for @{text
+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_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"},
+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
 \begin{isabelle}\ \ \ \ \ %%%
 @{text "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}\hfill\numbered{listequiv}
 \end{isabelle}
 @{text "\<union>"}, as list append.
 Quotients are important in a variety of areas, but they are really ubiquitous in
 the area of reasoning about programming language calculi. A simple example
 is the lambda-calculus, whose raw terms are defined as
+%
+%\begin{isabelle}\ \ \ \ \ %%%
-\begin{isabelle}\ \ \ \ \ %%%
+@{text "t ::= x | t t | \<lambda>x.t"}%\hfill\numbered{lambda}
-@{text "t ::= x | t t | \<lambda>x.t"}\hfill\numbered{lambda}
+%\end{isabelle}
-\end{isabelle}
+%
+%\noindent
-\noindent
 The problem with this definition arises, for instance, when one attempts to
 prove formally the substitution lemma \cite{Barendregt81} by induction
 over the structure of terms. This can be fiendishly complicated (see
 \cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof
 about raw lambda-terms). In contrast, if we reason about
 %%% Cezary: I like the diagram, maybe 'new type' could be outside, but otherwise
 %%% I wouldn't change it.
 \begin{center}
-\mbox{}\hspace{20mm}\begin{tikzpicture}
+\mbox{}\hspace{20mm}\begin{tikzpicture}[scale=0.9]
 %%\draw[step=2mm] (-4,-1) grid (4,1);
 \draw[very thick] (0.7,0.3) circle (4.85mm);
 \draw[rounded corners=1mm, very thick] ( 0.0,-0.9) rectangle ( 1.8, 0.9);
 \draw[rounded corners=1mm, very thick] (-1.95,0.8) rectangle (-2.9,-0.195);
 \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}};
 \draw (-0.95, 0.26) node[below=0.4mm] {@{text Abs}};
 \end{tikzpicture}
 \end{center}
 \noindent
 The starting point is an existing type, to which we refer as the
-\emph{raw type} and over which an equivalence relation given by the user is
+\emph{raw type} and over which an equivalence relation is given by the user.
-defined. With this input the package introduces a new type, to which we
+With this input the package introduces a new type, to which we
 refer as the \emph{quotient type}. This type comes with an
 \emph{abstraction} and a \emph{representation} function, written @{text Abs}
 and @{text Rep}.\footnote{Actually slightly more basic functions are given;
 the functions @{text Abs} and @{text Rep} need to be derived from them. We
 will show the details later. } They relate elements in the
-existing type to elements in the new type and vice versa, and can be uniquely
+existing type to elements in the new type, % and vice versa,
+and can be uniquely
 identified by their quotient type. For example for the integer quotient construction
 the types of @{text Abs} and @{text Rep} are
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm concat.simps(1)[THEN eq_reflection]}\hspace{10mm}
 @{thm concat.simps(2)[THEN eq_reflection, no_vars]}
 \end{isabelle}
 \noindent
-where @{text "@"} is the usual list append. We expect that the corresponding
+where @{text "@"} is %the usual
+list append. We expect that the corresponding
 operator on finite sets, written @{term "fconcat"},
 builds finite unions of finite sets:
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm concat_empty_fset[THEN eq_reflection, no_vars]}\hspace{10mm}
 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
+generate the %%%following
+definition
 \begin{isabelle}\ \ \ \ \ %%%
 @{text "\<Union> S \<equiv> Abs_fset (flat ((map_list Rep_fset \<circ> Rep_fset) S))"}
 \end{isabelle}
 It will also be necessary to have operators, referred to as @{text "rel_\<kappa>"},
 which define equivalence relations in terms of constituent equivalence
 relations. For example given two equivalence relations @{text "R\<^isub>1"}
 and @{text "R\<^isub>2"}, we can define an equivalence relations over
-products as follows
+products as %% follows
 \begin{isabelle}\ \ \ \ \ %%%
 @{text "(R\<^isub>1 \<tripple> R\<^isub>2) (x\<^isub>1, x\<^isub>2) (y\<^isub>1, y\<^isub>2) \<equiv> R\<^isub>1 x\<^isub>1 y\<^isub>1 \<and> R\<^isub>2 x\<^isub>2 y\<^isub>2"}
 \end{isabelle}
 with @{text R} being an equivalence relation, then
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{r@ {\hspace{1mm}}l}
 @{text  "Quot"} & @{text "(rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>)"}\\
-& @{text "(Abs_fset \<circ> map_list Abs)"}\\
+& @{text "(Abs_fset \<circ> map_list Abs)"} @{text "(map_list Rep \<circ> Rep_fset)"}\\
-& @{text "(map_list Rep \<circ> Rep_fset)"}\\
 \end{tabular}
 \end{isabelle}
 *}
 section {* Quotient Types and Quotient\\ Definitions\label{sec:type} *}
 %
 \begin{center}
 \hfill
 \begin{tabular}{@ {\hspace{2mm}}l@ {}}
 \multicolumn{1}{@ {}l}{equal types:}\\
-@{text "ABS (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\
+@{text "ABS (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\hspace{5mm}%\\
 @{text "REP (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\
 \multicolumn{1}{@ {}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{1}{@ {}l}{equal type constructors:}\\
 \noindent
 In our implementation we further
 simplify this function by rewriting with the usual laws about @{text
 "map"}s and @{text "id"}, for example @{term "map_list id = id"} and @{text "f \<circ> id =
-id \<circ> f = f"}. This gives us the simpler abstraction function
+id \<circ> f = f"}. This gives us %%%the simpler abstraction function
 \begin{isabelle}\ \ \ \ \ %%%
 @{text "(map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
 \end{isabelle}
 Note that by using the operator @{text "\<singlearr>"} and special clauses
 for function types in \eqref{ABSREP}, we do not have to
 distinguish between arguments and results, but can deal with them uniformly.
 Consequently, all definitions in the quotient package
 are of the general form
+%
-\begin{isabelle}\ \ \ \ \ %%%
+%\begin{isabelle}\ \ \ \ \ %%%
-@{text "c \<equiv> ABS (\<sigma>, \<tau>) t"}
+\mbox{@{text "c \<equiv> ABS (\<sigma>, \<tau>) t"}}
-\end{isabelle}
+%\end{isabelle}
+%
-\noindent
+%\noindent
 where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the
 type of the defined quotient constant @{text "c"}. This data can be easily
 generated from the declaration given by the user.
 To increase the confidence in this way of making definitions, we can prove
 that the terms involved are all typable.
 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
 can be given, \emph{not} all theorems can be lifted to the quotient type. Most
-notable is the bound variable function, that is the constant @{text bn}, defined
+notable is the bound variable function %%, that is the constant @{text bn},
+defined
 for raw lambda-terms as follows
 \begin{isabelle}
 \begin{center}
 @{text "bn (x) \<equiv> \<emptyset>"}\hspace{4mm}
 elsewhere.
 \begin{center}
 \hfill
 \begin{tabular}{l}
-\multicolumn{1}{@ {}l}{equal types:}\\
+\multicolumn{1}{@ {}l}{equal types:}
 @{text "REL (\<sigma>, \<sigma>)"} $\dn$ @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
 \multicolumn{1}{@ {}l}{equal type constructors:}\\
 @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
 \multicolumn{1}{@ {}l}{unequal type constructors:}\\
 @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} $\dn$ @{text "rel_\<kappa>\<^isub>q (REL (\<sigma>s', \<tau>s))"}\\
 Let us return to the lifting procedure of theorems. Assume we have a theorem
 that contains the raw constant @{text "c\<^isub>r :: \<sigma>"} and which we want to
 lift to a theorem where @{text "c\<^isub>r"} is replaced by the corresponding
 constant @{text "c\<^isub>q :: \<tau>"} defined over a quotient type. In this situation
 we generate the following proof obligation
+%
-\begin{isabelle}\ \ \ \ \ %%%
+%\begin{isabelle}\ \ \ \ \ %%%
-@{text "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
+@{text "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}.
-\end{isabelle}
+%\end{isabelle}
+%
-\noindent
+%\noindent
 Homeier calls these proof obligations \emph{respectfulness
 theorems}. However, unlike his quotient package, we might have several
 respectfulness theorems for one constant---he has at most one.
 The reason is that because of our quotient compositions, the types
 @{text \<sigma>} and @{text \<tau>} are not completely determined by @{text "c\<^bsub>r\<^esub>"}.
 And for every instantiation of the types, a corresponding
 respectfulness theorem is necessary.
 Before lifting a theorem, we require the user to discharge
 respectfulness proof obligations. In case of @{text bn}
-this obligation is as follows
+this obligation is %%as follows
+%
-\begin{isabelle}\ \ \ \ \ %%%
+%\begin{isabelle}\ \ \ \ \ %%%
 @{text  "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
-\end{isabelle}
+%\end{isabelle}
+%
-\noindent
+%\noindent
 and the point is that the user cannot discharge it: because it is not true. To see this,
 we can just unfold the definition of @{text "\<doublearr>"} \eqref{relfun}
 using extensionality to obtain the false statement
 \begin{isabelle}\ \ \ \ \ %%%
 @{text "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 then bn(t\<^isub>1) = bn(t\<^isub>2)"}
 \end{isabelle}
 \noindent
-In contrast, if we lift a theorem about @{text "append"} to a theorem describing
+In contrast, lifting a theorem about @{text "append"} to a theorem describing
-the union of finite sets, then we need to discharge the proof obligation
+the union of finite sets will mean to discharge the proof obligation
 \begin{isabelle}\ \ \ \ \ %%%
 @{text "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}
 \end{isabelle}
 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\\
+\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> Resp (REL (\<sigma>, \<tau>)). REG (t, s)"}
-\end{cases}$\smallskip\\
+\end{cases}$\\%%\smallskip\\
 \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> Resp (REL (\<sigma>, \<tau>)). REG (t, s)"}
-\end{cases}$\smallskip\\
+\end{cases}$\\%%\smallskip\\
-\multicolumn{1}{@ {}l@ {}}{equality:}\smallskip\\
+\multicolumn{1}{@ {}l@ {}}{equality:  \hspace{3mm}%%}\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:}\\
 @{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}
 useful in the new version of Nominal Isabelle, where such a choice is
 required to generate a reasoning infrastructure for alpha-equated terms.
 %%
 %% give an example for this
 %%
-\medskip
+\smallskip
 \noindent
 {\bf Acknowledgements:} We would like to thank Peter Homeier for the many
-discussions about his HOL4 quotient package and explaining to us
+discussions about his HOL4 quotient package.\\[-5mm]% and explaining to us
-some of its finer points in the implementation. Without his patient
+%some of its finer points in the implementation. Without his patient
-help, this work would have been impossible.
+%help, this work would have been impossible.
 %  \appendix
 *}

changeset 2554	2668486b684a
parent 2553	ea0cdb7c6455
child 2558	6cfb5d8a5b5b