nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:b51532dd5689
+:bcb037806e16
 theory Paper
 imports "Quotient"
 "LaTeXsugar"
 "../Nominal/FSet"
 begin
+(****
+** things to do for the next version
+*
+* - what are quot_thms?
+* - what do all preservation theorems look like,
+in particular preservation for quotient
+compositions
+*)
 notation (latex output)
 rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
 pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
 "op -->" (infix "\<longrightarrow>" 100) and
 @{text "\<sigma>s"} to stand for collections of type variables and types,
 respectively.  The type of a term is often made explicit by writing @{text
 "t :: \<sigma>"}. HOL includes a type @{typ bool} for booleans and the function
 type, written @{text "\<sigma> \<Rightarrow> \<tau>"}. HOL also contains many primitive and defined
 constants; a primitive constant is equality, with type @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
-bool"}, and the identity function with type @{text "id :: \<sigma> => \<sigma>"} is
+bool"}, and the identity function with type @{text "id :: \<sigma> \<Rightarrow> \<sigma>"} is
 defined as @{text "\<lambda>x\<^sup>\<sigma>. x\<^sup>\<sigma>"}).
 An important point to note is that theorems in HOL can be seen as a subset
-of terms that are constructed specially (namely through axioms and prove
+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
 First, a general quotient theorem, like the one given in Proposition \ref{funquot},
 cannot be stated inside HOL, because of the restriction on types.
 Second, even if we were able to state such a quotient theorem, it
 would not be true in general. However, we can prove specific instances of a
 quotient theorem for composing particular quotient relations.
-To lift @{term flat} the quotient theorem for composing @{text "\<approx>\<^bsub>list\<^esub>"}
+For example, to lift theorems involving @{term flat} the quotient theorem for
-is necessary:
+composing @{text "\<approx>\<^bsub>list\<^esub>"} will be necessary: given @{term "Quotient R Abs Rep"}
-% It says when lists are being quotiented to finite sets,
+with @{text R} being an equivalence relation, then
-% the contents of the lists can be quotiented as well
-If @{term R} is an equivalence relation and @{term "Quotient R Abs Rep"} then
+@{text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep \<circ> rep_fset)"}
-@{text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep o rep_fset)"}
 \vspace{-.5mm}
 *}
 section {* Quotient Types and Quotient Definitions\label{sec:type} *}
 text {*
 respectively.  Given that @{text "R"} is an equivalence relation, the
 following property holds  for every quotient type
 (for the proof see \cite{Homeier05}).
 \begin{proposition}
-@{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
+@{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.
 \end{proposition}
 The next step in a quotient construction is to introduce definitions of new constants
 involving the quotient type. These definitions need to be given in terms of concepts
 of the raw type (remember this is the only way how to extend HOL
 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 the 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
-notably 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}\ \ \ \ \ \ \ \ \ \ %%%
 @{text "bn (x) \<equiv> \<emptyset>"}\hspace{4mm}
 @{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{4mm}
 the properties of \emph{respectfulness} and \emph{preservation}. We have
 to slightly extend Homeier's definitions in order to deal with quotient
 compositions.
 To formally define what respectfulness is, we have to first define
-the notion of \emph{aggregate equivalence relations} using @{text REL}:
+the notion of \emph{aggregate equivalence relations} using the function @{text REL}:
 \begin{center}
 \hfill
 \begin{tabular}{rcl}
 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
 Lets 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 throw the following proof obligation
+we generate the following proof obligation
 @{text [display, indent=10] "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
-%%% PROBLEM I do not yet completely understand the
+\noindent
-%%% form of respectfulness theorems
-%%%\noindent
-%%%if @ {text \<sigma>} and @ {text \<tau>} have no type variables. In case they have, then
-%%%the proof obligation is of the form
-%%%
-%%%@ {text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub>  implies  REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
-%%% ANSWER: The respectfulness theorems never have any quotient assumptions,
-%%% So the commited version is ok.
-\noindent
-%%%where @ {text "\<alpha>s"} are the type variables in @{text \<sigma>} and @{text \<tau>}.
 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 the type of @{text "c\<^bsub>r\<^esub>"}.
 And for every instantiation of the types, we might end up with a
 corresponding respectfulness theorem.
 Before lifting a theorem, we require the user to discharge
-them. And the point with @{text bn} is that the respectfulness theorem
+respectfulness proof obligations. And the point with @{text bn} is that the respectfulness theorem
 looks as follows
 @{text [display, indent=10] "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
 \noindent
-and the user cannot discharge it---because it is not true. To see this,
+and 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 extensionally to obtain
 @{text [display, indent=10] "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 implies bn(t\<^isub>1) = bn(t\<^isub>2)"}
 \noindent
 To do so, we have to establish
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-if @{thm (prem1) append_rsp_unfolded[of xs ys us vs, no_vars]} and
+if @{text "xs \<approx>\<^bsub>list\<^esub> ys"} and  @{text "us \<approx>\<^bsub>list\<^esub> vs"}
-@{thm (prem2) append_rsp_unfolded[of xs ys us vs, no_vars]}
+then @{text "xs @ us \<approx>\<^bsub>list\<^esub> ys @ vs"}
-then @{thm (concl) append_rsp_unfolded[of xs ys us vs, no_vars]}
 \end{isabelle}
 \noindent
 which is straightforward given the definition shown in \eqref{listequiv}.
 The second restriction we have to impose arises from
 non-lifted polymorphic constants, which are instantiated to a
-type being quotient. For example, take the @{term "cons"} to
+type being quotient. For example, take the @{term "cons"}-constructor to
-add a pair of natural numbers to a list. The pair of natural numbers
+add a pair of natural numbers to a list, whereby teh pair of natural numbers
-is to become an integer. But we still want to use @{text cons} for
+is to become an integer in te quotient construction. The point is that we
+still want to use @{text cons} for
 adding integers to lists---just with a different type.
-To be able to lift such theorems, we need a \emph{preservation theorem}
+To be able to lift such theorems, we need a \emph{preservation property}
 for @{text cons}. Assuming we have a polymorphic raw constant
 @{text "c\<^isub>r :: \<sigma>"} and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"},
-then a preservation theorem 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"}.
 \noindent
 under the assumption @{text "Quotient R Abs Rep"}. Interestingly, if we have
 an instance of @{text cons} where the type variable @{text \<alpha>} is instantiated
 with @{text "nat \<times> nat"} and we also quotient this type to yield integers,
-then we need to show the corresponding preservation lemma.
+then we need to show the corresponding preservation property.
 %%%@ {thm [display, indent=10] insert_preserve2[no_vars]}
 %Given two quotients, one of which quotients a container, and the
 %other quotients the type in the container, we can write the
 text {*
 The main benefit of a quotient package is to lift automatically theorems over raw
 types to theorems over quotient types. We will perform this lifting in
 three phases, called \emph{regularization},
-\emph{injection} and \emph{cleaning}.
+\emph{injection} and \emph{cleaning} according to procedures in Homeier's ML-code.
 The purpose of regularization is to change the quantifiers and abstractions
 in a ``raw'' theorem to quantifiers over variables that respect the relation
 (Definition \ref{def:respects} states what respects means). The purpose of injection is to add @{term Rep}
 and @{term Abs} of appropriate types in front of constants and variables
 3.) & @{text "inj_thm \<longleftrightarrow> quot_thm"}\\
 \end{tabular}
 \end{center}
 \noindent
+which means the raw theorem implies the quotient theorem.
 In contrast to other quotient packages, our package requires
 the \emph{term} of the @{text "quot_thm"} to be given by the user.\footnote{Though we
 also provide a fully automated mode, where the @{text "quot_thm"} is guessed
-from @{text "raw_thm"}.} As a result, it is possible that a user can lift only some
+from the form of @{text "raw_thm"}.} As a result, it is possible that a user can lift only some
-occurrences of a raw type.
+occurrences of a raw type, but not others.
 The second and third proof step will always succeed if the appropriate
 respectfulness and preservation theorems are given. In contrast, the first
 proof step can fail: a theorem given by the user does not always
 imply a regularized version and a stronger one needs to be proved. This
 is outside of the scope where the quotient package can help. An example
-for the failure is the simple statement for integers @{text "0 \<noteq> 1"}.
+for this kind of failure is the simple statement for integers @{text "0 \<noteq> 1"}.
-It does not follow by lifting from the fact that @{text "(0, 0) \<noteq> (1, 0)"}.
+One might hope that it can be proved by lifting @{text "(0, 0) \<noteq> (1, 0)"},
-The raw theorem only shows that particular element in the
+but the raw theorem only shows that particular element in the
-equivalence classes are not equal. A more general statement saying that
+equivalence classes are not equal. A more general statement stipulating that
-the equivalence classes are not equal is necessary.
+the equivalence classes are not equal is necessary, and then leads to the
+theorem  @{text "0 \<noteq> 1"}.
 In the following we will first define the statement of the
 regularized theorem based on @{text "raw_thm"} and
 @{text "quot_thm"}. Then we define the statement of the injected theorem, based
-on @{text "reg_thm"} theorem and @{text "quot_thm"}. We then show the 3 proofs,
+on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps,
 which can all be performed independently from each other.
-We define the function @{text REG}. The intuition
+We first define the function @{text REG}. The intuition
 behind this function is that it replaces quantifiers and
 abstractions involving raw types by bounded ones, and equalities
 involving raw types are replaced by appropriate aggregate
 equivalence relations. It is defined as follows:
 \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 universal quantifier. For the third and fourt 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"}:
 In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always
 start with an implication. Isabelle provides \emph{mono} rules that can split up
 the implications into simpler implication subgoals. This succeeds for every
 monotone connective, except in places where the function @{text REG} inserted,
-for example, a quantifier by a bounded quantifier. In this case we have
+for instance, a quantifier by a bounded quantifier. In this case we have
 rules of the form
 @{text [display, indent=10] "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}
 \noindent
 @{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
 \noindent
 The last theorem is new in comparison with Homeier's package. There the
-injection procedure would be used to prove such goals, and there
+injection procedure would be used to prove such goals, and
 the assumption about the equivalence relation would be used. We use the above theorem directly,
 because this allows us to completely separate the first and the second
-proof step into independent ``units''.
+proof step into two independent ``units''.
 The second proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"},  starts with an equality.
 The proof again follows the structure of the
 two underlying terms, and is defined for a goal being a relation between these two terms.
 \end{itemize}
 We defined the theorem @{text "inj_thm"} in such a way that
 establishing the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be
 achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient
-definitions. Then all lifted constants, their definitions
+definitions. Then for all lifted constants, their definitions
 are used to fold the @{term Rep} with the raw constant. Next for
 all abstractions and quantifiers the lambda and
 quantifier preservation theorems are used to replace the
 variables that include raw types with respects by quantifiers
 over variables that include quotient types. We show here only
 The user can then specify the constants on the quotient type:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
 \begin{tabular}{@ {}l}
 \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\[3mm]
-\isacommand{fun}~~@{text "plus_raw"}~~\isacommand{where}~~%
+\isacommand{fun}~~@{text "add_pair"}~~\isacommand{where}~~%
-@{text "plus_raw (m, n) (p, q) = (m + p :: nat, n + q :: nat)"}\\
+@{text "add_pair (m, n) (p, q) \<equiv> (m + p :: nat, n + q :: nat)"}\\
 \isacommand{quotient\_definition}~~@{text "+ :: int \<Rightarrow> int \<Rightarrow> int"}~~%
-\isacommand{is}~~@{text "plus_raw"}\\
+\isacommand{is}~~@{text "add_pair"}\\
 \end{tabular}
 \end{isabelle}
 \noindent
 The following theorem about addition on the raw level can be proved.
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
-\isacommand{lemma}~~@{text "plus_zero_raw: int_rel (plus_raw (0, 0) x) x"}
+\isacommand{lemma}~~@{text "add_pair_zero: int_rel (add_pair (0, 0) x) x"}
 \end{isabelle}
 \noindent
 If the user attempts to lift this theorem, all proof obligations are
 automatically discharged, except the respectfulness
-proof for @{text "plus_raw"}:
+proof for @{text "add_pair"}:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
 \begin{tabular}{@ {}l}
-\isacommand{lemma}~~@{text "[quot_respect]:\\
+\isacommand{lemma}~~@{text "[quot_respect]:"}\\
-(int_rel \<doublearr> int_rel \<doublearr> int_rel) plus_raw plus_raw"}
+@{text "(int_rel \<doublearr> int_rel \<doublearr> int_rel) add_pair add_pair"}
 \end{tabular}
 \end{isabelle}
 \noindent
 This can be discharged automatically by Isabelle when telling it to unfold the definition
 of @{text "\<doublearr>"}.
 After this, the user can prove the lifted lemma explicitly:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
-\isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting plus_zero_raw"}
+\isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting add_pair_zero"}
 \end{isabelle}
 \noindent
 or by the completely automated mode by stating:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
-\isacommand{thm}~~@{text "plus_zero_raw[quot_lifted]"}
+\isacommand{thm}~~@{text "add_pair_zero[quot_lifted]"}
 \end{isabelle}
 \noindent
 Both methods give the same result, namely
 @{text [display, indent=10] "0 + x = x"}
 \noindent
 Although seemingly simple, arriving at this result without the help of a quotient
-package requires substantial reasoning effort.
+package requires a substantial reasoning effort.
 *}
 section {* Conclusion and Related Work\label{sec:conc}*}
 text {*
 The code of the quotient package and the examples described here are
 already included in the
 standard distribution of Isabelle.\footnote{Available from
 \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 convenient reasoning
-infrastructure for programming language calculi involving binders.
+infrastructure for programming language calculi involving general binders.
 To achieve this, it builds types representing @{text \<alpha>}-equivalent terms.
 Earlier
 versions of Nominal Isabelle have been used successfully in formalisations
 of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08},
 Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for
 Paulson showed a construction of quotients that does not require the
 Hilbert Choice operator, but also only first-order theorems can be lifted~\cite{Paulson06}.
 The most related work to our package is the package for HOL4 by Homeier~\cite{Homeier05}.
 He introduced most of the abstract notions about quotients and also deals with the
 lifting of higher-order theorems. However, he cannot deal with quotient compositions (needed
-for lifting theorems about @{text flat}. Also, a number of his definitions, like @{text ABS},
+for lifting theorems about @{text flat}). Also, a number of his definitions, like @{text ABS},
-@{text REP} and @{text INJ} etc only exist in ML-code. On the other hand, Homeier
+@{text REP} and @{text INJ} etc only exist in \cite{Homeier05} as ML-code, not included
-is able to deal with partial quotient constructions, which we have not implemented.
+in the paper.
 One advantage of our package is that it is modular---in the sense that every step
 in the quotient construction can be done independently (see the criticism of Paulson
 about other quotient packages). This modularity is essential in the context of
 Isabelle, which supports type-classes and locales.
-Another feature of our quotient package is that when lifting theorems, we can
+Another feature of our quotient package is that when lifting theorems, teh user can
 precisely specify what the lifted theorem should look like. This feature is
-necessary, for example, when lifting an inductive principle about two lists.
+necessary, for example, when lifting an induction principle for two lists.
 This principle has as the conclusion a predicate of the form @{text "P xs ys"},
 and we can precisely specify whether we want to quotient @{text "xs"} or @{text "ys"},
 or both. We found this feature very useful in the new version of Nominal
-Isabelle.
+Isabelle, where such a choice is required to generate a resoning infrastructure
+for alpha-equated terms.
+%%
+%% give an example for this
+%%
 \medskip
 \noindent
-{\bf Acknowledgements:} We would like to thank Peter Homeier for the
+{\bf Acknowledgements:} We would like to thank Peter Homeier for the many
 discussions about his HOL4 quotient package and explaining to us
-some of its finer points in the implementation.
+some of its finer points in the implementation. Without his patient
+help, this work would have been impossible.
 *}

changeset 2327	bcb037806e16
parent 2287	adb5b1349280
child 2319	7c8783d2dcd0