nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:46be4145b922
+:34af7f2ca490
 cumbersome and inelegant in light of our work, which can deal with such
 definitions directly. The solution is that we need to build aggregate
 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>"},
 according to the type of the raw constant and the type
 of the quotient constant. This means we also have to extend the notions
 rules). As a result we are able to define automatic proof
 procedures showing that one theorem implies another by decomposing the term
 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
 @{thm [display, indent=10] fun_map_def[no_vars, THEN eq_reflection]}
 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"}
 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}
 *}
 section {* Quotient Types and Quotient Definitions\label{sec:type} *}
 @{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
 @{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
 \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
+"\<rho>s \<kappa>"} 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
+substitutions for the @{text "\<alpha>s"} when matching  @{text "\<sigma>s \<kappa>"} against
-@{text "\<sigma>s \<kappa>"}.  The
+@{text "\<rho>s \<kappa>"}.  The
 function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw
 type as follows:
 %
 \begin{center}
 \begin{tabular}{rcl}
 The need for aggregate map-functions can be seen in cases where we build quotients,
 say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}.
 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
 abstraction and representation functions.
 example about @{term "concat"} and @{term "fconcat"}, where we have the raw type
 @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and the quotient type @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>
 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
 for function types in \eqref{ABSREP}, we do not have to
 distinguish between arguments and results, but can deal with them uniformly.
 \begin{tabular}{rcl}
 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
 @{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}
 \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
 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
 \noindent
 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
 an instance of @{text cons} where the type variable @{text \<alpha>} is instantiated
 with @{text "nat \<times> nat"} and we also quotient this type to yield integers,
 %theorem which allows quotienting inside the container:
 %
 %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
 %%%injection and cleaning proofs allowing the lifting procedure to
 %%%proceed in an unchanged way.

changeset 2367	34af7f2ca490
parent 2366	46be4145b922
child 2369	3aeb58524131