nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:dceaf2d9fedd
+:63f0e7f914dd
 \noindent
 where we take the representation of the arguments @{text n} and @{text m},
 add them according to the function @{text "add_pair"} and then take the
 abstraction of the result.  This is all straightforward and the existing
-quotient packages can deal with such definitions. But what is surprising
+quotient packages can deal with such definitions. But what is surprising is
 that none of them can deal with slightly more complicated definitions involving
 \emph{compositions} of quotients. Such compositions are needed for example
 in case of quotienting lists to yield finite sets and the operator that
 flattens lists of lists, defined as follows
 @{text [display, indent=10] "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
 \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 extensionally to obtain the false statement
+using extensionality 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)"}
+@{text [display, indent=10] "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 then bn(t\<^isub>1) = bn(t\<^isub>2)"}
 \noindent
 In contrast, if we lift a theorem about @{text "append"} to a theorem describing
 the union of finite sets, then we need to discharge the proof obligation
 types to theorems over quotient types. We will perform this lifting in
 three phases, called \emph{regularization},
 \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
+in a ``raw'' theorem to quantifiers over variables that respect their respective relations
 (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 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
 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
-If @{term R\<^isub>2} is an equivalence relation, we can prove
+If @{term R\<^isub>2} is an equivalence relation, we can prove that for any predicate @{term P}
 @{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
 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 second proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"},  starts with an equality
+between the terms of the regularized theorem and the injected theorem.
 The proof again follows the structure of the
 two underlying terms and is defined for a goal being a relation between these two terms.
 \begin{itemize}
 \item For two constants an appropriate respectfulness theorem is applied.
 \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 for all lifted constants, their definitions
+definitions. Next the definitions of all lifted constants
-are used to fold the @{term Rep} with the raw constant. Next for
+are used to fold the @{term Rep} with the raw constants. 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 lambda preservation theorem. Given
 @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}, we have:
 @{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.
+Next, relations over lifted types can be rewritten to equalities
-For this the following theorem has been shown by  Homeier~\cite{Homeier05}:
+over lifted type. Rewriting is performed with the following theorem,
+which 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

changeset 2412	63f0e7f914dd
parent 2377	273f57049bd1
child 2413	1341a2d7570f