nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:781fbc8c0591
+:6cfb5d8a5b5b
 @{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}
-%\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
 $\alpha$-equated lambda-terms, that means terms quotient according to
 $\alpha$-equivalence, then the reasoning infrastructure provided,
-for example, by Nominal Isabelle %\cite{UrbanKaliszyk11}
+for example, by Nominal Isabelle %%\cite{UrbanKaliszyk11}
 makes the formal
 proof of the substitution lemma almost trivial.
 The difficulty is that in order to be able to reason about integers, finite
 sets or $\alpha$-equated lambda-terms one needs to establish a reasoning
 @{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
+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}\ \ \ \ \ %%%
 following the structure of the theorem being lifted and the theorem
 on the quotient level. Space constraints, unfortunately, allow us to only
 sketch this part of our work in Section 5 and we defer the reader to a longer
 version for the details. However, we will give in Section 3 and 4 all
 definitions that specify the input and output data of our three-step
-lifting procedure.
+lifting procedure. Appendix A gives an example how our quotient
-%Appendix A gives an example how our quotient package works in practise.
+package works in practise.
 *}
 section {* Preliminaries and General\\ Quotients\label{sec:prelims} *}
 text {*
 \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}\ \ \ \ \ %%%
 \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},
+notable is the bound variable function, that is the constant @{text bn},
 defined
 for raw lambda-terms as follows
 \begin{isabelle}
 \begin{center}
 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"}.
-%\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>"}.
 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
-%
-%\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}\ \ \ \ \ %%%
 %%
 \smallskip
 \noindent
 {\bf Acknowledgements:} We would like to thank Peter Homeier for the many
-discussions about his HOL4 quotient package.\\[-5mm]% and explaining to us
+discussions about his HOL4 quotient package 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
 *}
-(* section {* Examples \label{sec:examples} *}
+text_raw {*
+%%\bibliographystyle{abbrv}
+\bibliography{root}
+\appendix
+*}
+section {* Examples \label{sec:examples} *}
 text {*
 %%% FIXME Reviewer 1 would like an example of regularized and injected
 %%% statements. He asks for the examples twice, but I would still ignore
 Both methods give the same result, namely @{text "0 + x = x"}
 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 (see \cite{Paulson06}).
 *}
-*)
 (*<*)
 end
 (*>*)

changeset 2558	6cfb5d8a5b5b
parent 2554	2668486b684a
child 2747	a5da7b6aff8f