nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:ba068c04a8d9
+:f5f21feaa168
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 @{text "t ::= x | t t | \<lambda>x.t"}\hfill\numbered{lambda}
 \end{isabelle}
 \noindent
-The problem with this definition arises when one attempts to
+The problem with this definition arises, for instance, when one attempts to
-prove formally, for example, the substitution lemma \cite{Barendregt81} by induction
+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
 $\alpha$-equated lambda-terms, that means terms quotient according to
 $\alpha$-equivalence, then the reasoning infrastructure provided,
 \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. } These functions relate elements in the
 existing type to elements in the new type and vice versa; they can be uniquely
-identified by their type. For example for the integer quotient construction
+identified by their quotient 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"}
 builds finite unions 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
+The quotient package should automatically provide us with a definition for @{text "\<Union>"} in
 terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is
 that the method  used in the existing quotient
 packages of just taking the representation of the arguments and then taking
 the abstraction of the result is \emph{not} enough. The reason is that case in case
 of @{text "\<Union>"} we obtain the incorrect definition
 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. Our
 quotient package is the first one that is modular so that it allows to lift
 single 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 needs to be
+the modularity is that we are able to clearly specify what is involved
-done in the lifting process (this was only hinted at in \cite{Homeier05} and
+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 respectfullness
-and preservation.\ldots
+and preservation; Section \ref{sec:lift} describes the lifting of theorems,
+and Section \ref{sec:conc} concludes and compares our results to existing
+work.
 *}
 section {* Preliminaries and General Quotient\label{sec:prelims} *}
 text {*
-In this section we present the definitions of a quotient that follow
+We describe here briefly some of the most basic concepts of HOL
-closely those given by Homeier.
+we rely on and some of the important definitions given by Homeier
+\cite{Homeier05}.
+HOL is based on a simply-typed term-language, where types are
+annotated in Church-style (that is we can obtain immediately
+infer the type of term and its subterms).
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+\begin{tabular}{@ {}rl@ {\hspace{3mm}}l@ {}}
+@{text "\<sigma>, \<tau> ::="} & @{text "\<alpha> | (\<sigma>,\<dots>, \<sigma>) \<kappa>"} & (type variables and type constructors)\\
+@{text "t, s ::="} & @{text "x\<^isup>\<sigma> | c\<^isup>\<sigma> | t t | \<lambda>x\<^isup>\<sigma>. t"} &
+(variables, constants, applications and abstractions)\\
+\end{tabular}
+\end{isabelle}
+\noindent
+We often write just @{text \<kappa>} for @{text "() \<kappa>"}, and use @{text "\<alpha>s"} and
+@{text "\<sigma>s"} to stand for list of type variables and types, respectively.
+The type of a term is often made explicit by writing @{text "t :: \<sigma>"} HOL
+contains a type @{typ bool} for booleans and the function type, written
+@{text "\<sigma> \<Rightarrow> \<tau>"}.
 \begin{definition}[Quotient]
 A relation $R$ with an abstraction function $Abs$
 and a representation function $Rep$ is a \emph{quotient}
 if and only if:
 \end{lemma}
 Higher Order Logic
-Types:
-\begin{eqnarray}\nonumber
-@{text "\<sigma> ::="} & @{text "\<alpha>"} & \textrm{(type variable)} \\ \nonumber
-@{text "|"} & @{text "(\<sigma>,\<dots>,\<sigma>)\<kappa>"} & \textrm{(type construction)}
-\end{eqnarray}
-Terms:
-\begin{eqnarray}\nonumber
-@{text "t ::="} & @{text "x\<^isup>\<sigma>"} & \textrm{(variable)} \\ \nonumber
-@{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 }
 Such maps for most common types (list, pair, sum,
 option, \ldots) are described in Homeier, and we assume that @{text "map"}
 is the function that returns a map for a given type.
 proceed in an unchanged way.
 *}
-section {* Lifting of Theorems *}
+section {* Lifting of Theorems\label{sec:lift} *}
 text {*
 The core of our quotient package takes an original theorem that
 talks about the raw types and the statement of the theorem that
 it is supposed to produce. This is different from existing
 \noindent
 obtaining the same result.
 *}
-section {* Related Work *}
+section {* Conclusion and Related Work\label{sec:conc}*}
 text {*
-\begin{itemize}
+\begin{itemize}
 \item Peter Homeier's package~\cite{Homeier05} (and related work from there)
 \item John Harrison's one~\cite{harrison-thesis} is the first one to lift theorems
 but only first order.
 \item Necessity of Hilbert Choice op and Larry's quotients~\cite{Paulson06}
 \item Setoids in Coq and \cite{ChicliPS02}
 \end{itemize}
-*}
-section {* Conclusion *}
-text {*
 The code of the quotient package described here is already included in the
 standard distribution of Isabelle.\footnote{Available from
 \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is

changeset 2256	f5f21feaa168
parent 2255	ba068c04a8d9
child 2257	d40031f786f0