nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:2d6cada7d5e0
+:ea7c3f21d6df
 text {*
 A respectfulness lemma for a constant states that the equivalence
 class returned by this constant depends only on the equivalence
-classes of the arguments applied to the constant. This can be
+classes of the arguments applied to the constant. To automatically
-expressed in terms of an aggregate relation between the constant
+lift a theorem that talks about a raw constant, to a theorem about
-and itself, for example the respectfullness for @{term "append"}
+the quotient type a respectfulness theorem is required.
+A respectfulness condition for a constant can be expressed in
+terms of an aggregate relation between the constant and itself,
+for example the respectfullness for @{term "append"}
 can be stated as:
 @{thm [display] append_rsp[no_vars]}
 \noindent
-Which is equivalent to:
+Which after unfolding @{term "op ===>"} is equivalent to:
 @{thm [display] append_rsp_unfolded[no_vars]}
-Below we show the algorithm for finding the aggregate relation.
+An aggregate relation is defined in terms of relation composition,
-This algorithm uses
+so we define it first:
-the relation composition which we define as:
 \begin{definition}[Composition of Relations]
 @{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate
 composition @{thm pred_compI[no_vars]}
 \end{definition}
-Given an aggregate raw type and quotient type:
+The aggregate relation for an aggregate raw type and quotient type
+is defined as:
 \begin{itemize}
-\item For equal types or free type variables return equality
+\item @{text "REL(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "op ="}
+\item @{text "REL(\<sigma>, \<sigma>)"}  =  @{text "op ="}
-\item For equal type constructors use the appropriate rel
+\item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(rel \<kappa>) (REL(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REL(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
-function applied to the results for the argument pairs
+\item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "(rel \<kappa>\<^isub>1) (REL(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REL(\<rho>\<^isub>p,\<nu>\<^isub>p) OOO Eqv_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
-\item For unequal type constructors, look in the quotients information
-for a quotient type that matches the type constructor, and instantiate
-the type appropriately getting back an instantiation environment. We
-apply the environment to the arguments and recurse composing it with
-the aggregate relation function.
 \end{itemize}
-Again, the the behaviour of our algorithm in the last situation is
+Again, the last case is novel, so lets look at the example of
-novel, so lets look at the example of respectfullness for @{term concat}.
+respectfullness for @{term concat}. The statement according to
-The statement as computed by the algorithm above is:
+the definition above is:
 @{thm [display] concat_rsp[no_vars]}
 \noindent
 By unfolding the definition of relation composition and relation map
 text {*
 Given two quotients, one of which quotients a container, and the
 other quotients the type in the container, we can write the
 composition of those quotients. To compose two quotient theorems
-we compose the relations with relation composition
+we compose the relations with relation composition as defined above
-and the abstraction and relation functions with function composition.
+and the abstraction and relation functions are the ones of the sub
-The @{term "Rep"} and @{term "Abs"} functions that we obtain are
+quotients composed with the usual function composition.
-the same as the ones created by in the aggregate functions and the
+The @{term "Rep"} and @{term "Abs"} functions that we obtain agree
+with the definition of aggregate Abs/Rep functions and the
 relation is the same as the one given by aggregate relations.
 This becomes especially interesting
 when we compose the quotient with itself, as there is no simple
 intermediate step.
 Lets take again the example of @{term concat}. To be able to lift
-theorems that talk about it we will first prove the composition
+theorems that talk about it we provide the composition quotient
-quotient theorems, which then lets us perform the lifting procedure
+theorems, which then lets us perform the lifting procedure in an
-in an unchanged way:
+unchanged way:
 @{thm [display] quotient_compose_list[no_vars]}
 *}
 text {*
 The core of the quotient package takes an original theorem that
 talks about the raw types, and the statement of the theorem that
 it is supposed to produce. This is different from other existing
-quotient packages, where only the raw theorems was necessary.
+quotient packages, where only the raw theorems were necessary.
 We notice that in some cases only some occurrences of the raw
 types need to be lifted. This is for example the case in the
 new Nominal package, where a raw datatype that talks about
 pairs of natural numbers or strings (being lists of characters)
 should not be changed to a quotient datatype with constructors
 implementation.
 We first define the statement of the regularized theorem based
 on the original theorem and the goal theorem. Then we define
 the statement of the injected theorem, based on the regularized
-theorem and the goal. We then show the 3 proofs, and all three
+theorem and the goal. We then show the 3 proofs as all three
 can be performed independently from each other.
 *}
 subsection {* Regularization and Injection statements *}
 text {*
-The function that gives the statement of the regularized theorem
+We first define the function @{text REG}, which takes the statements
-takes the statement of the raw theorem (a term) and the statement
+of the raw theorem and the lifted theorem (both as terms) and
-of the lifted theorem. The intuition behind the procedure is that
+returns the statement of the regularized version. The intuition
-it replaces quantifiers and abstractions involving raw types
+behind this function is that it replaces quantifiers and
-by bounded ones, and equalities involving raw types are replaced
+abstractions involving raw types by bounded ones, and equalities
-by appropriate aggregate relations. It is defined as follows:
+involving raw types are replaced by appropriate aggregate
+relations. It is defined as follows:
 \begin{itemize}
 \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"}
 \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
 \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"}
 \item @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}
 \item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"}
 \item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"}
 \end{itemize}
-Existential quantifiers and unique existential quantifiers are defined
+In the above definition we ommited the cases for existential quantifiers
-similarily to the universal one.
+and unique existential quantifiers, as they are very similar to the cases
+for the universal quantifier.
-The function that gives the statment of the injected theorem
-takes the statement of the regularized theorems and the statement
+Next we define the function @{text INJ} which takes the statement of
-of the lifted theorem both as terms.
+the regularized theorems and the statement of the lifted theorem both as
+terms and returns the statment of the injected theorem:
 \begin{itemize}
 \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"}
 \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"}
 \item @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"}

changeset 2207	ea7c3f21d6df
parent 2206	2d6cada7d5e0
child 2208	b0b2198040d7