--- a/Quotient-Paper/Paper.thy Thu May 27 18:37:52 2010 +0200
+++ b/Quotient-Paper/Paper.thy Thu May 27 18:40:10 2010 +0200
@@ -1,7 +1,9 @@
+
(*<*)
theory Paper
imports "Quotient"
"LaTeXsugar"
+ "../Nominal/FSet"
begin
notation (latex output)
@@ -10,6 +12,8 @@
fun_map ("_ ---> _" [51, 51] 50)
and
fun_rel ("_ ===> _" [51, 51] 50)
+and
+ list_eq (infix "\<approx>" 50) (* Not sure if we want this notation...? *)
ML {*
fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;
@@ -75,18 +79,19 @@
surprising, none of them can deal compositions of quotients, for example with
lifting theorems about @{text "concat"}:
- @{thm concat.simps(1)}\\
- @{thm concat.simps(2)[no_vars]}
+ @{thm [display] concat.simps(1)}
+ @{thm [display] concat.simps(2)[no_vars]}
\noindent
- One would like to lift this definition to the operation
-
- @{text [display] "union definition"}
+ One would like to lift this definition to the operation:
+
+ @{thm [display] fconcat_empty[no_vars]}
+ @{thm [display] fconcat_insert[no_vars]}
\noindent
What is special about this operation is that we have as input
lists of lists which after lifting turn into finite sets of finite
- sets.
+ sets.
*}
subsection {* Contributions *}
@@ -101,7 +106,7 @@
\item We define quotient composition, function map composition and
relation map composition. This lets lifting polymorphic types with
subtypes quotiented as well. We extend the notions of
- respectfullness and preservation to cope with quotient
+ respectfulness and preservation to cope with quotient
composition.
\item We allow lifting only some occurrences of quotiented
@@ -140,8 +145,8 @@
\end{definition}
- \begin{definition}[Relation map and function map]
- @{thm fun_rel_def[no_vars]}\\
+ \begin{definition}[Relation map and function map]\\
+ @{thm fun_rel_def[of "R1" "R2", no_vars]}\\
@{thm fun_map_def[no_vars]}
\end{definition}
@@ -153,75 +158,303 @@
*}
-section {* Constants *}
-
-(* Describe what containers are? *)
+subsection {* Higher Order Logic *}
text {*
- \begin{definition}[Composition of Relations]
- @{abbrev "rel_conj R1 R2"}
- \end{definition}
+
+ Types:
+ \begin{eqnarray}\nonumber
+ @{text "\<sigma> ::="} & @{text "\<alpha>"} & \textrm{(type variable)} \\ \nonumber
+ @{text "|"} & @{text "(\<sigma>,\<dots>,\<sigma>)\<kappa>"} & \textrm{(type construction)}
+ \end{eqnarray}
+
+ Terms:
+ \begin{eqnarray}\nonumber
+ @{text "t ::="} & @{text "x\<^isup>\<sigma>"} & \textrm{(variable)} \\ \nonumber
+ @{text "|"} & @{text "c\<^isup>\<sigma>"} & \textrm{(constant)} \\ \nonumber
+ @{text "|"} & @{text "t t"} & \textrm{(application)} \\ \nonumber
+ @{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber
+ \end{eqnarray}
+
+*}
- The first operation that we describe is the generation of
- aggregate Abs or Rep function for two given compound types.
- This operation will be used for the constant defnitions
- and for the translation of theorems statements. It relies on
- knowing map functions and relation functions for container types.
- It follows the following algorithm:
+section {* Constants *}
+
+(* Say more about containers? *)
+
+text {*
+
+ To define a constant on the lifted type, an aggregate abstraction
+ function is applied to the raw constant. Below we describe the operation
+ that generates
+ an aggregate @{term "Abs"} or @{term "Rep"} function given the
+ compound raw type and the compound quotient type.
+ This operation will also be used in translations of theorem statements
+ and in the lifting procedure.
+
+ The operation is additionally able to descend into types for which
+ maps are known. Such maps for most common types (list, pair, sum,
+ option, \ldots) are described in Homeier, and we assume that @{text "map"}
+ is the function that returns a map for a given type. Then REP/ABS is defined
+ as follows:
\begin{itemize}
- \item For equal types or free type variables return identity.
-
- \item For function types recurse, change the Rep/Abs flag to
- the opposite one for the domain type and compose the
- results with @{term "fun_map"}.
-
- \item For equal type constructors use the appropriate map function
- applied to the results for the arguments.
-
- \item For unequal type constructors are unequal, we look in the
- quotients information for a raw type quotient type pair that
- matches the given types. We apply the environment to the arguments
- and recurse composing it with the aggregate map function.
+ \item @{text "ABS(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "id"}
+ \item @{text "REP(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "id"}
+ \item @{text "ABS(\<sigma>, \<sigma>)"} = @{text "id"}
+ \item @{text "REP(\<sigma>, \<sigma>)"} = @{text "id"}
+ \item @{text "ABS(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"} = @{text "REP(\<sigma>\<^isub>1,\<tau>\<^isub>1) ---> ABS(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
+ \item @{text "REP(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"} = @{text "ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1) ---> REP(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
+ \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"} = @{text "(map \<kappa>) (ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (ABS(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
+ \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"} = @{text "(map \<kappa>) (REP(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REP(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
+ \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"} = @{text "Abs_\<kappa>\<^isub>2 \<circ> (map \<kappa>\<^isub>1) (ABS(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (ABS(\<rho>\<^isub>p,\<nu>\<^isub>p)"} 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 @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"} = @{text "(map \<kappa>\<^isub>1) (REP(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REP(\<rho>\<^isub>p,\<nu>\<^isub>p) \<circ> Rep_\<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"}
\end{itemize}
+ Apart from the last 2 points the definition is same as the one implemented in
+ in Homeier's HOL package, below is the definition of @{term fconcat}
+ that shows the last points:
+ @{thm fconcat_def[no_vars]}
+
+ The aggregate @{term Abs} function takes a finite set of finite sets
+ and applies @{term "map rep_fset"} composed with @{term rep_fset} to
+ its input, obtaining a list of lists, passes the result to @{term concat}
+ obtaining a list and applies @{term abs_fset} obtaining the composed
+ finite set.
+*}
+
+subsection {* Respectfulness *}
+
+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
+ 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:
+
+ @{thm [display] append_rsp_unfolded[no_vars]}
+
+ Below we show the algorithm for finding the aggregate relation.
+ This algorithm uses
+ 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:
+
+ \begin{itemize}
+ \item For equal types or free type variables return equality
+
+ \item For equal type constructors use the appropriate rel
+ function applied to the results for the argument pairs
+
+ \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
+ novel, so lets look at the example of respectfullness for @{term concat}.
+ The statement as computed by the algorithm above is:
- Rsp and Prs
+ @{thm [display] concat_rsp[no_vars]}
+
+ \noindent
+ By unfolding the definition of relation composition and relation map
+ we can see the equivalent statement just using the primitive list
+ equivalence relation:
+
+ @{thm [display] concat_rsp_unfolded[of "a" "a'" "b'" "b", no_vars]}
+
+ The statement reads that, for any lists of lists @{term a} and @{term b}
+ if there exist intermediate lists of lists @{term "a'"} and @{term "b'"}
+ such that each element of @{term a} is in the relation with an appropriate
+ element of @{term a'}, @{term a'} is in relation with @{term b'} and each
+ element of @{term b'} is in relation with the appropriate element of
+ @{term b}.
+
*}
+subsection {* Preservation *}
+
+text {*
+ To be able to lift theorems that talk about constants that are not
+ lifted but whose type changes when lifting is performed additionally
+ preservation theorems are needed.
+
+ To lift theorems that talk about insertion in lists of lifted types
+ we need to know that for any quotient type with the abstraction and
+ representation functions @{text "Abs"} and @{text Rep} we have:
+
+ @{thm [display] (concl) cons_prs[no_vars]}
+
+ This is not enough to lift theorems that talk about quotient compositions.
+ For some constants (for example empty list) it is possible to show a
+ general compositional theorem, but for @{term "op #"} it is necessary
+ to show that it respects the particular quotient type:
+
+ @{thm [display] insert_preserve2[no_vars]}
+*}
+
+subsection {* Composition of Quotient theorems *}
+
+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
+ and the abstraction and relation functions with function composition.
+ The @{term "Rep"} and @{term "Abs"} functions that we obtain are
+ the same as the ones created by in the aggregate 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
+ quotient theorems, which then lets us perform the lifting procedure
+ in an unchanged way:
+
+ @{thm [display] quotient_compose_list[no_vars]}
+*}
+
+
section {* Lifting Theorems *}
-text {* TBD *}
+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.
+ 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
+ taking integers or finite sets of characters. To simplify the
+ use of the quotient package we additionally provide an automated
+ statement translation mechanism that replaces occurrences of
+ types that match given quotients by appropriate lifted types.
-text {* Why providing a statement to prove is necessary is some cases *}
+ Lifting the theorems is performed in three steps. In the following
+ we call these steps \emph{regularization}, \emph{injection} and
+ \emph{cleaning} following the names used in Homeier's HOL
+ implementation.
-subsection {* Regularization *}
+ 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
+ can be performed independently from each other.
+
+*}
+
+subsection {* Regularization and Injection statements *}
text {*
-Transformation of the theorem statement:
-\begin{itemize}
-\item Quantifiers and abstractions involving raw types replaced by bounded ones.
-\item Equalities involving raw types replaced by bounded ones.
-\end{itemize}
+
+ The function that gives the statement of the regularized theorem
+ takes the statement of the raw theorem (a term) and the statement
+ of the lifted theorem. The intuition behind the procedure is that
+ it replaces quantifiers and abstractions involving raw types
+ by bounded ones, and equalities involving raw types are replaced
+ by appropriate aggregate relations. It is defined as follows:
-The procedure.
+ \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 (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
+ \item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"}
+ \item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"}
+ \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
+ similarily to the universal one.
+
+ The function that gives the statment of the injected theorem
+ takes the statement of the regularized theorems and the statement
+ of the lifted theorem both as terms.
-Example of non-regularizable theorem ($0 = 1$).
+ \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))))"}
+ \item @{text "INJ (\<forall> t, \<forall> s) = \<forall> (INJ (t, s)"}
+ \item @{text "INJ (\<forall> t \<in> R, \<forall> s) = \<forall> (INJ (t, s) \<in> R"}
+ \item @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}
+ \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) = v\<^isub>1"}
+ \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"}
+ \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) = c\<^isub>1"}
+ \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"}
+ \end{itemize}
+
+ For existential quantifiers and unique existential quantifiers it is
+ defined similarily to the universal one.
+
+*}
+
+subsection {* Proof of Regularization *}
-Separtion of regularization from injection thanks to the following 2 lemmas:
-\begin{lemma}
-If @{term R2} is an equivalence relation, then:
-\begin{eqnarray}
-@{thm (rhs) ball_reg_eqv_range[no_vars]} & = & @{thm (lhs) ball_reg_eqv_range[no_vars]}\\
-@{thm (rhs) bex_reg_eqv_range[no_vars]} & = & @{thm (lhs) bex_reg_eqv_range[no_vars]}
-\end{eqnarray}
-\end{lemma}
+text {*
+ Example of non-regularizable theorem ($0 = 1$).
+
+
+ Separtion of regularization from injection thanks to the following 2 lemmas:
+ \begin{lemma}
+ If @{term R2} is an equivalence relation, then:
+ \begin{eqnarray}
+ @{thm (rhs) ball_reg_eqv_range[no_vars]} & = & @{thm (lhs) ball_reg_eqv_range[no_vars]}\\
+ @{thm (rhs) bex_reg_eqv_range[no_vars]} & = & @{thm (lhs) bex_reg_eqv_range[no_vars]}
+ \end{eqnarray}
+ \end{lemma}
+
+ Other lemmas used in regularization:
+ @{thm [display] ball_reg_eqv[no_vars]}
+ @{thm [display] bex_reg_eqv[no_vars]}
+ @{thm [display] babs_reg_eqv[no_vars]}
+ @{thm [display] babs_simp[no_vars]}
+
+ @{thm [display] ball_reg_right[no_vars]}
+ @{thm [display] bex_reg_left[no_vars]}
+ @{thm [display] bex1_bexeq_reg[no_vars]}
*}
subsection {* Injection *}
+text {*
+
+ The 2 key lemmas are:
+
+ @{thm [display] apply_rsp[no_vars]}
+ @{thm [display] rep_abs_rsp[no_vars]}
+
+
+
+*}
+
+
+
+
subsection {* Cleaning *}
text {* Preservation of quantifiers, abstractions, relations, quotient-constants