nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:f170ee51eed2
+:9a560e489c64
 of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}
 from Homeier \cite{Homeier05}.
 In addition we are able to address the criticism by Paulson \cite{Paulson06} cited
 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
+lifted from the raw level to the quotient level into one giant list. Homeier's and
-quotient package is the first one that is modular so that it allows to lift
+also our quotient package are modular so that they allow lifting
-single higher-order theorems separately. This has the advantage for the user of being able to develop a
+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 is involved
 in the lifting process (this was only hinted at in \cite{Homeier05} and
 implemented as a ``rough recipe'' in ML-code).
 We often write just @{text \<kappa>} for @{text "() \<kappa>"}, and use @{text "\<alpha>s"} 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>
+constants; for example, a primitive constant is equality, with type @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
 bool"}, and the identity function with type @{text "id :: \<sigma> \<Rightarrow> \<sigma>"} is
-defined as @{text "\<lambda>x\<^sup>\<sigma>. x\<^sup>\<sigma>"}).
+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 proof
 rules). As a result we are able to define automatic proof
 procedures showing that one theorem implies another by decomposing the term
 @{thm [display, indent=10] fun_map_def[no_vars, THEN eq_reflection]}
 \noindent
 Using this map-function, we can give the following, equivalent, but more
-uniform, definition for @{text add} shown in \eqref{adddef}:
+uniform definition for @{text add} shown in \eqref{adddef}:
 @{text [display, indent=10] "add \<equiv> (Rep_int \<singlearr> Rep_int \<singlearr> Abs_int) add_pair"}
 \noindent
 Using extensionality and unfolding the definition of @{text "\<singlearr>"},
 \item @{thm (rhs3) Quotient_def[of "R", no_vars]}
 \end{enumerate}
 \end{definition}
 \noindent
-The value of this definition is that validity of @{text "Quotient R Abs Rep"} can
+The value of this definition lies in the fact that validity of @{text "Quotient R Abs Rep"} can
 often be proved in terms of the validity of @{text "Quotient"} over the constituent
 types of @{text "R"}, @{text Abs} and @{text Rep}.
 For example Homeier proves the following property for higher-order quotient
 types:
 \end{definition}
 \noindent
 Unfortunately, there are two predicaments with compositions of relations.
 First, a general quotient theorem, like the one given in Proposition \ref{funquot},
-cannot be stated inside HOL, because of the restriction on types.
+cannot be stated inside HOL, because of restrictions 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.
 For example, to lift theorems involving @{term flat} the quotient theorem for
 composing @{text "\<approx>\<^bsub>list\<^esub>"} will be necessary: given @{term "Quotient R Abs Rep"}
 The first one declares zero for integers and the second the operator for
 building unions of finite sets (@{text "flat"} having the type
 @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"}).
 The problem for us is that from such declarations we need to derive proper
-definitions using the @{text "Abs"} and @{text "Rep"} functions for the
+definitions using @{text "Abs"} and @{text "Rep"}. The data we rely on is the given quotient type
-quotient types involved. The data we rely on is the given quotient type
 @{text "\<tau>"} and the raw type @{text "\<sigma>"}.  They allow us to define \emph{aggregate
 abstraction} and \emph{representation functions} using the functions @{text "ABS (\<sigma>,
-\<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses we give below. The idea behind
+\<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses we shall give below. The idea behind
 these two functions is to simultaneously descend into the raw types @{text \<sigma>} and
 quotient types @{text \<tau>}, and generate the appropriate
 @{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore
 we generate just the identity whenever the types are equal. On the ``way'' down,
 however we might have to use map-functions to let @{text Abs} and @{text Rep} act
 over the appropriate types. In what follows we use the short-hand notation
-@{text "ABS (\<sigma>s, \<tau>s)"} to mean @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1)\<dots>ABS (\<sigma>\<^isub>i, \<tau>\<^isub>i)"}; similarly
+@{text "ABS (\<sigma>s, \<tau>s)"} to mean @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1)\<dots>ABS (\<sigma>\<^isub>n, \<tau>\<^isub>n)"}; similarly
 for @{text REP}.
 %
 \begin{center}
 \hfill
 \begin{tabular}{rcl}
 text {*
 The main point of the quotient package is to automatically ``lift'' theorems
 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
+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}, defined
 for raw lambda-terms as follows
 The @{text "\<sigma>s'"} in the last clause are calculated as in \eqref{ABSREP}:
 we know that type @{text "\<alpha>s \<kappa>\<^isub>q"} is the quotient of the raw type
 @{text "\<rho>s \<kappa>"}. The @{text "\<sigma>s'"} are determined by matching
 @{text "\<rho>s \<kappa>"} and @{text "\<sigma>s \<kappa>"}.
-Lets return to the lifting procedure of theorems. Assume we have a theorem
+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
 @{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
-respectfulness proof obligations. And the point with @{text bn} is that the respectfulness theorem
+respectfulness proof obligations. In case of @{text bn}
-looks as follows
+this obligation is 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 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 extensionally to obtain
+using extensionally to obtain the false statement
 @{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
 In contrast, if we lift a theorem about @{text "append"} to a theorem describing
 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"}-constructor to
-add a pair of natural numbers to a list, whereby teh pair of natural numbers
+add a pair of natural numbers to a list, whereby the pair of natural numbers
-is to become an integer in te quotient construction. The point is that we
+turns into an integer in the 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 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>"},
 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
-of the raw type so that they can be replaced by the ones that include the
+of the raw type so that they can be replaced by the corresponding constants from the
 quotient type. The purpose of cleaning is to bring the theorem derived in the
 first two phases into the form the user has specified. Abstractly, our
 package establishes the following three proof steps:
 \begin{center}
 quantifiers.
 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 implicational subgoals. This succeeds for every
-monotone connective, except in places where the function @{text REG} inserted,
+monotone connective, except in places where the function @{text REG} replaced,
 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)"}
 relation. If @{text R} is an equivalence relation we can prove that
 @{text [display, indent=10] "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}
 \noindent
-And when @{term R\<^isub>2} is an equivalence relation and we can prove
+If @{term R\<^isub>2} is an equivalence relation, we can prove
 @{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
+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 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.
+two underlying terms and is defined for a goal being a relation between these two terms.
 \begin{itemize}
-\item For two constants an appropriate constant respectfulness lemma is applied.
+\item For two constants an appropriate respectfulness theorem is applied.
 \item For two variables, we use the assumptions proved in the regularization step.
 \item For two abstractions, we @{text "\<eta>"}-expand and @{text "\<beta>"}-reduce them.
 \item For two applications, we check that the right-hand side is an application of
-@{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"}. If yes then we
+@{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"} holds. If yes then we
 can apply the theorem:
 @{term [display, indent=10] "R x y \<longrightarrow> R x (Rep (Abs y))"}
 Otherwise we introduce an appropriate relation between the subterms
 @{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
 \noindent
 Next, relations over lifted types are folded to equalities.
-For this the following theorem has been shown in Homeier~\cite{Homeier05}:
+For this the following theorem has been shown by  Homeier~\cite{Homeier05}:
 @{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]}
 \noindent
 Finally, we rewrite with the preservation theorems. This will result
 (* Mention why equivalence *)
 text {*
-In this section we will show, a complete interaction with the quotient package
+In this section we will show a sequence of declarations for defining the
-for defining the type of integers by quotienting pairs of natural numbers and
+type of integers by quotienting pairs of natural numbers, and
-lifting theorems to integers. Our quotient package is fully compatible with
+lifting one theorem.
-Isabelle type classes, but for clarity we will not use them in this example.
-In a larger formalization of integers using the type class mechanism would
-provide many algebraic properties ``for free''.
 A user of our quotient package first needs to define a relation on
-the raw type, by which the quotienting will be performed. We give
+the raw type with which the quotienting will be performed. We give
 the same integer relation as the one presented in \eqref{natpairequiv}:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
 \begin{tabular}{@ {}l}
 \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"}\\
 \isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"}
 \end{tabular}
 \end{isabelle}
 \noindent
-Next the quotient type is defined. This generates a proof obligation that the
+Next the quotient type must be defined. This generates a proof obligation that the
 relation is an equivalence relation, which is solved automatically using the
-definition and extensionality:
+definition of equivalence and extensionality:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
 \begin{tabular}{@ {}l}
 \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"}\\
 \hspace{5mm}@{text "by (auto simp add: equivp_def expand_fun_eq)"}
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
 \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
+If the user lifts this theorem, all proof obligations are
 automatically discharged, except the respectfulness
 proof for @{text "add_pair"}:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
 \begin{tabular}{@ {}l}
 @{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
+This property needs to beproved 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 explicitly:
+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 the completely automated mode by stating:
+or by using the completely automated stating just:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
 \isacommand{thm}~~@{text "add_pair_zero[quot_lifted]"}
 \end{isabelle}
 in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02},
 and setoids in Coq \cite{ChicliPS02}.
 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
+He introduced most of the abstract notions about quotients and also deals with
 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},
 @{text REP} and @{text INJ} etc only exist in \cite{Homeier05} as ML-code, not included
 in the paper.
-One advantage of our package is that it is modular---in the sense that every step
+One feature of our quotient package is that when lifting theorems, the user can
-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, teh user can
 precisely specify what the lifted theorem should look like. This feature is
 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"},
+Assuming 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"},
+then 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, where such a choice is required to generate a resoning infrastructure
 for alpha-equated terms.
 %%
 %% give an example for this

changeset 2332	9a560e489c64
parent 2319	7c8783d2dcd0
child 2333	a0fecce8b244