--- a/Quotient-Paper/Paper.thy Sat Jul 17 12:01:04 2010 +0100
+++ b/Quotient-Paper/Paper.thy Sat Jul 17 15:44:24 2010 +0100
@@ -243,10 +243,10 @@
representation and abstraction functions, which in case of @{text "\<Union>"}
generate the following definition
- @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat ((map Rep_fset \<circ> Rep_fset) S))"}
+ @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat ((map_list Rep_fset \<circ> Rep_fset) S))"}
\noindent
- where @{term map} is the usual mapping function for lists. In this paper we
+ where @{term map_list} is the usual mapping function for lists. In this paper we
will present a formal definition of our aggregate abstraction and
representation functions (this definition was omitted in \cite{Homeier05}).
They generate definitions, like the one above for @{text "\<Union>"},
@@ -312,7 +312,7 @@
underlying the first theorem.
Like Homeier's, our work relies on map-functions defined for every type
- constructor taking some arguments, for example @{text map} for lists. Homeier
+ constructor taking some arguments, for example @{text map_list} for lists. Homeier
describes in \cite{Homeier05} map-functions for products, sums, options and
also the following map for function types
@@ -414,7 +414,7 @@
composing @{text "\<approx>\<^bsub>list\<^esub>"} will be necessary: given @{term "Quotient R Abs Rep"}
with @{text R} being an equivalence relation, then
- @{text [display, indent=10] "Quotient (rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (Abs_fset \<circ> map Abs) (map Rep \<circ> Rep_fset)"}
+ @{text [display, indent=2] "Quotient (rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (Abs_fset \<circ> map_list Abs) (map_list Rep \<circ> Rep_fset)"}
\vspace{-.5mm}
*}
@@ -543,20 +543,21 @@
\multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\
@{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\
@{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\
- \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\
+ \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors with @{text "\<alpha>s
+ \<kappa>\<^isub>q"} being the quotient of the raw type @{text "\<rho>s \<kappa>"}:}\\
@{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s)))"}\\
@{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s))) \<circ> Rep_\<kappa>\<^isub>q"}
\end{tabular}\hfill\numbered{ABSREP}
\end{center}
%
\noindent
- In the last two clauses we have that the type @{text "\<alpha>s
+ In the last two clauses we rely on the fact that the type @{text "\<alpha>s
\<kappa>\<^isub>q"} is the quotient of the raw type @{text "\<rho>s \<kappa>"} (for example
@{text "int"} and @{text "nat \<times> nat"}, or @{text "\<alpha> fset"} and @{text "\<alpha>
list"}). The quotient construction ensures that the type variables in @{text
- "\<rho>s"} must be among the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
- matchers for the @{text "\<alpha>s"} when matching @{text "\<rho>s \<kappa>"} against
- @{text "\<sigma>s \<kappa>"}. The
+ "\<rho>s \<kappa>"} must be among the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
+ substitutions for the @{text "\<alpha>s"} when matching @{text "\<sigma>s \<kappa>"} against
+ @{text "\<rho>s \<kappa>"}. The
function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw
type as follows:
%
@@ -579,7 +580,7 @@
In this case @{text MAP} generates the
aggregate map-function:
- @{text [display, indent=10] "\<lambda>a b. map_prod (map a) b"}
+ @{text [display, indent=10] "\<lambda>a b. map_prod (map_list a) b"}
\noindent
which is essential in order to define the corresponding aggregate
@@ -591,20 +592,20 @@
fset"}. Feeding these types into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)
the abstraction function
- @{text [display, indent=10] "(map (map id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map id"}
+ @{text [display, indent=10] "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map_list id"}
\noindent
In our implementation we further
simplify this function by rewriting with the usual laws about @{text
- "map"}s and @{text "id"}, namely @{term "map id = id"} and @{text "f \<circ> id =
+ "map"}s and @{text "id"}, for example @{term "map_list id = id"} and @{text "f \<circ> id =
id \<circ> f = f"}. This gives us the simpler abstraction function
- @{text [display, indent=10] "(map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
+ @{text [display, indent=10] "(map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
\noindent
which we can use for defining @{term "fconcat"} as follows
- @{text [display, indent=10] "\<Union> \<equiv> ((map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}
+ @{text [display, indent=10] "\<Union> \<equiv> ((map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}
\noindent
Note that by using the operator @{text "\<singlearr>"} and special clauses
@@ -686,7 +687,8 @@
@{text "REL (\<sigma>, \<sigma>)"} & $\dn$ & @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\
@{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
- \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\smallskip\\
+ \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors with @{text "\<alpha>s
+ \<kappa>\<^isub>q"} being the quotient of the raw type @{text "\<rho>s \<kappa>"}:}\smallskip\\
@{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "rel_\<kappa>\<^isub>q (REL (\<sigma>s', \<tau>s))"}\\
\end{tabular}\hfill\numbered{REL}
\end{center}
@@ -694,7 +696,7 @@
\noindent
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>"}. The @{text "\<sigma>s'"} are the substitutions for @{text "\<alpha>s"} obtained by matching
@{text "\<rho>s \<kappa>"} and @{text "\<sigma>s \<kappa>"}.
Let us return to the lifting procedure of theorems. Assume we have a theorem
@@ -762,7 +764,7 @@
where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}.
In case of @{text cons} (which has type @{text "\<alpha> \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"}) we have
- @{text [display, indent=10] "(Rep ---> map Rep ---> map Abs) cons = cons"}
+ @{text [display, indent=10] "(Rep ---> map_list Rep ---> map_list Abs) cons = cons"}
\noindent
under the assumption @{text "Quotient R Abs Rep"}. Interestingly, if we have
@@ -792,7 +794,7 @@
%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 o rep_fset)"}
+ %@ {text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map_list Abs) (map_list Rep o rep_fset)"}
%%%
%%%\noindent
%%%this theorem will then instantiate the quotients needed in the