nominal2: comparison Quotient-Paper-jv/Paper.thy

equal deleted inserted replaced

-:578e0265b235
+:9e7047159f43
 \noindent
 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
+terms of operations on pairs of natural numbers:
-"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)"}).
+\begin{isabelle}\ \ \ \ \ %%%
-Similarly one can construct %%the type of
+@{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)"}
+\end{isabelle}
+\noindent
+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}
 $\alpha$-equated lambda-terms, that means terms quotient according to
 $\alpha$-equivalence, then the reasoning infrastructure provided,
 for example, by Nominal Isabelle %%\cite{UrbanKaliszyk11}
 makes the formal
 proof of the substitution lemma almost trivial.
+{\bf MAYBE AN EAMPLE FOR PARTIAL QUOTIENTS?}
 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
 infrastructure by transferring, or \emph{lifting}, definitions and theorems
 from the raw type @{typ "nat \<times> nat"} to the quotient type @{typ int}
 according to the type of the raw constant and the type
 of the quotient constant. This means we also have to extend the notions
 of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}
 from Homeier \cite{Homeier05}.
+{\bf EXAMPLE BY HUFFMAN ABOUT @{thm map_concat}}
 In addition we are able to clearly specify what is involved
 in the lifting process (this was only hinted at in \cite{Homeier05} and
 implemented as a ``rough recipe'' in ML-code). A pleasing side-result
 is that our procedure for lifting theorems is completely deterministic
 following the structure of the theorem being lifted and the theorem
-on the quotient level. Space constraints, unfortunately, allow us to only
+on the quotient level. {\it 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
+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. Appendix A gives an example how our quotient
 package works in practise.
 *}
-section {* Preliminaries and General\\ Quotients\label{sec:prelims} *}
+section {* Preliminaries and General Quotients\label{sec:prelims} *}
 text {*
 \noindent
 We will give in this section a crude overview of HOL and describe the main
 definitions given by Homeier for quotients \cite{Homeier05}.
 & @{text "(Abs_fset \<circ> map_list Abs)"} @{text "(map_list Rep \<circ> Rep_fset)"}\\
 \end{tabular}
 \end{isabelle}
 *}
-section {* Quotient Types and Quotient\\ Definitions\label{sec:type} *}
+section {* Quotient Types and Quotient Definitions\label{sec:type} *}
 text {*
 \noindent
 The first step in a quotient construction is to take a name for the new
 type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},
 equivalent to @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}, which we just have to compose with
 @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"} according to the type of @{text "\<circ>"}.\qed
 \end{proof}
 *}
-section {* Respectfulness and\\ Preservation \label{sec:resp} *}
+section {* Respectfulness and Preservation \label{sec:resp} *}
 text {*
 \noindent
 The main point of the quotient package is to automatically ``lift'' theorems
 involving constants over the raw type to theorems involving constants over
 LF \cite{UrbanCheneyBerghofer08}, Typed
 Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
 \cite{BengtsonParow09} and a strong normalisation result for cut-elimination
 in classical logic \cite{UrbanZhu08}.
+{\bf INSTEAD OF NOMINAL WORK, GIVE WORK BY BULWAHN ET AL?}
 There is a wide range of existing literature for dealing with quotients
 in theorem provers.  Slotosch~\cite{Slotosch97} implemented a mechanism that
 automatically defines quotient types for Isabelle/HOL. But he did not
 include theorem lifting.  Harrison's quotient package~\cite{harrison-thesis}
 \noindent
 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}).
+{\bf \begin{itemize}
+\item Type maps and Relation maps (show the case for functions)
+\item Quotient extensions
+\item Respectfulness and preservation
+- Show special cases for quantifiers and lambda
+\item Quotient-type locale
+- Show the proof as much simpler than Homeier's one
+\item ??? Infrastructure for storing theorems (rsp, prs, eqv, quot and idsimp)
+\item Lifting vs Descending vs quot\_lifted
+- automatic theorem translation heuristic
+\item Partial equivalence quotients
+- Bounded abstraction
+- Respects
+- partial descending
+\item The heuristics for automatic regularization, injection and cleaning.
+\item A complete example of a lifted theorem together with the regularized
+injected and cleaned statement
+\item Examples of quotients and properties that we used the package for.
+\item co/contra-variance from Ondrej should be taken into account
+\end{itemize}}
 *}
 (*<*)

changeset 3095	9e7047159f43
parent 3094	8bad9887ad90
child 3114	a9a4baa7779f