nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:9a560e489c64
+:a0fecce8b244
 *
 * - what are quot_thms?
 * - what do all preservation theorems look like,
 in particular preservation for quotient
 compositions
+- explain how Quotient R Abs Rep is proved (j-version)
+- give an example where precise specification helps (core Haskell in nominal?)
 *)
 notation (latex output)
 rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
 pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
 of terms that are constructed specially (namely through axioms and proof
 rules). As a result we are able to define automatic proof
 procedures showing that one theorem implies another by decomposing the term
 underlying the first theorem.
-Like Homeier, our work relies on map-functions defined for every type
+Like Homeier's, our work relies on map-functions defined for every type
 constructor taking some arguments, for example @{text map} for lists. Homeier
 describes in \cite{Homeier05} map-functions for products, sums, options and
 also the following map for function types
 @{thm [display, indent=10] fun_map_def[no_vars, THEN eq_reflection]}
 \noindent
 As a result, Homeier is able to build an automatic prover that can nearly
 always discharge a proof obligation involving @{text "Quotient"}. Our quotient
 package makes heavy
 use of this part of Homeier's work including an extension
-to deal with compositions of equivalence relations defined as follows:
+for dealing with compositions of equivalence relations defined as follows:
 \begin{definition}[Composition of Relations]
 @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate
 composition defined by
 @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
 \end{isabelle}
 \noindent
 which is straightforward given the definition shown in \eqref{listequiv}.
-The second restriction we have to impose arises from
+The second restriction we have to impose arises from non-lifted polymorphic
-non-lifted polymorphic constants, which are instantiated to a
+constants, which are instantiated to a type being quotient. For example,
-type being quotient. For example, take the @{term "cons"}-constructor to
+take the @{term "cons"}-constructor to add a pair of natural numbers to a
-add a pair of natural numbers to a list, whereby the pair of natural numbers
+list, whereby we assume the pair of natural numbers turns into an integer in
-turns into an integer in the quotient construction. The point is that we
+the quotient construction. The point is that we still want to use @{text
-still want to use @{text cons} for
+cons} for adding integers to lists---just with a different type. To be able
-adding integers to lists---just with a different type.
+to lift such theorems, we need a \emph{preservation property} for @{text
-To be able to lift such theorems, we need a \emph{preservation property}
+cons}. Assuming we have a polymorphic raw constant @{text "c\<^isub>r :: \<sigma>"}
-for @{text cons}. Assuming we have a polymorphic raw constant
+and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"}, then a
-@{text "c\<^isub>r :: \<sigma>"} and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"},
+preservation property is as follows
-then a preservation property is as follows
 @{text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies  ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"}
 \noindent
 where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}.
 \end{center}
 %
 \noindent
 In the above definition we omitted the cases for existential quantifiers
 and unique existential quantifiers, as they are very similar to the cases
-for the universal quantifier. For the third and fourt clause, note that
+for the universal quantifier. For the third and fourth clause, note that
 @{text "\<forall>x. P"} is defined as @{text "\<forall> (\<lambda>x. P)"}.
 Next we define the function @{text INJ} which takes as argument
 @{text "reg_thm"} and @{text "quot_thm"} (both as
 terms) and returns @{text "inj_thm"}:
 @{text "(int_rel \<doublearr> int_rel \<doublearr> int_rel) add_pair add_pair"}
 \end{tabular}
 \end{isabelle}
 \noindent
-This property needs to beproved by the user. It
+This property needs to be proved by the user. It
 can be discharged automatically by Isabelle when hinting to unfold the definition
 of @{text "\<doublearr>"}.
 After this, the user can prove the lifted lemma as follows:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
 \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting add_pair_zero"}
 \end{isabelle}
 \noindent
-or by using the completely automated stating just:
+or by using the completely automated mode stating just:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
 \isacommand{thm}~~@{text "add_pair_zero[quot_lifted]"}
 \end{isabelle}
 Both methods give the same result, namely
 @{text [display, indent=10] "0 + x = x"}
 \noindent
+where @{text x} is of type integer.
 Although seemingly simple, arriving at this result without the help of a quotient
-package requires a substantial reasoning effort.
+package requires a substantial reasoning effort (see \cite{Paulson06}).
 *}
 section {* Conclusion and Related Work\label{sec:conc}*}
 text {*
-The code of the quotient package and the examples described here are
+The code of the quotient package and the examples described here are already
-already included in the
+included in the standard distribution of Isabelle.\footnote{Available from
-standard distribution of Isabelle.\footnote{Available from
+\href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} The package is
-\href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is
+heavily used in the new version of Nominal Isabelle, which provides a
-heavily used in the new version of Nominal Isabelle, which provides a convenient reasoning
+convenient reasoning infrastructure for programming language calculi
-infrastructure for programming language calculi involving general binders.
+involving general binders.  To achieve this, it builds types representing
-To achieve this, it builds types representing @{text \<alpha>}-equivalent terms.
+@{text \<alpha>}-equivalent terms.  Earlier versions of Nominal Isabelle have been
-Earlier
+used successfully in formalisations of an equivalence checking algorithm for
-versions of Nominal Isabelle have been used successfully in formalisations
+LF \cite{UrbanCheneyBerghofer08}, Typed
-of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08},
+Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
-Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for
+\cite{BengtsonParow09} and a strong normalisation result for cut-elimination
-concurrency \cite{BengtsonParow09} and a strong normalisation result for
+in classical logic \cite{UrbanZhu08}.
-cut-elimination in classical logic \cite{UrbanZhu08}.
-There is a wide range of existing of literature for dealing with
+There is a wide range of existing literature for dealing with quotients
-quotients in theorem provers.
+in theorem provers.  Slotosch~\cite{Slotosch97} implemented a mechanism that
-Slotosch~\cite{Slotosch97} implemented a mechanism that automatically
+automatically defines quotient types for Isabelle/HOL. But he did not
-defines quotient types for Isabelle/HOL. But he did not include theorem lifting.
+include theorem lifting.  Harrison's quotient package~\cite{harrison-thesis}
-Harrison's quotient package~\cite{harrison-thesis} is the first one that is
+is the first one that is able to automatically lift theorems, however only
-able to automatically lift theorems, however only first-order theorems (that is theorems
+first-order theorems (that is theorems where abstractions, quantifiers and
-where abstractions, quantifiers and variables do not involve functions that
+variables do not involve functions that include the quotient type). There is
-include the quotient type).
+also some work on quotient types in non-HOL based systems and logical
-There is also some work on quotient types in
+frameworks, including theory interpretations in
-non-HOL based systems and logical frameworks, including theory interpretations
+PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, and
-in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02},
+setoids in Coq \cite{ChicliPS02}.  Paulson showed a construction of
-and setoids in Coq \cite{ChicliPS02}.
+quotients that does not require the Hilbert Choice operator, but also only
-Paulson showed a construction of quotients that does not require the
+first-order theorems can be lifted~\cite{Paulson06}.  The most related work
-Hilbert Choice operator, but also only first-order theorems can be lifted~\cite{Paulson06}.
+to our package is the package for HOL4 by Homeier~\cite{Homeier05}.  He
-The most related work to our package is the package for HOL4 by Homeier~\cite{Homeier05}.
+introduced most of the abstract notions about quotients and also deals with
-He introduced most of the abstract notions about quotients and also deals with
+lifting of higher-order theorems. However, he cannot deal with quotient
-lifting of higher-order theorems. However, he cannot deal with quotient compositions (needed
+compositions (needed for lifting theorems about @{text flat}). Also, a
-for lifting theorems about @{text flat}). Also, a number of his definitions, like @{text ABS},
+number of his definitions, like @{text ABS}, @{text REP} and @{text INJ} etc
-@{text REP} and @{text INJ} etc only exist in \cite{Homeier05} as ML-code, not included
+only exist in \cite{Homeier05} as ML-code, not included in the paper.
-in the paper.
-One feature of our quotient package is that when lifting theorems, the user can
+One feature of our quotient package is that when lifting theorems, the user
-precisely specify what the lifted theorem should look like. This feature is
+can precisely specify what the lifted theorem should look like. This feature
-necessary, for example, when lifting an induction principle for two lists.
+is necessary, for example, when lifting an induction principle for two
-Assuming this principle has as the conclusion a predicate of the form @{text "P xs ys"},
+lists.  Assuming this principle has as the conclusion a predicate of the
-then we can precisely specify whether we want to quotient @{text "xs"} or @{text "ys"},
+form @{text "P xs ys"}, then we can precisely specify whether we want to
-or both. We found this feature very useful in the new version of Nominal
+quotient @{text "xs"} or @{text "ys"}, or both. We found this feature very
-Isabelle, where such a choice is required to generate a resoning infrastructure
+useful in the new version of Nominal Isabelle, where such a choice is
-for alpha-equated terms.
+required to generate a reasoning infrastructure for alpha-equated terms.
 %%
 %% give an example for this
 %%
 \medskip

changeset 2333	a0fecce8b244
parent 2332	9a560e489c64
child 2334	0d10196364aa