83   One would like to lift this definition to the operation

    85   One would like to lift this definition to the operation:

    84   

    86 

    85   @{text [display] "union definition"}

    87   @{thm fconcat_empty[no_vars]}\\

    88   @{thm fconcat_insert[no_vars]}

   105     respectfullness and preservation to cope with quotient

   108     respectfulness and preservation to cope with quotient

   144   \begin{definition}[Relation map and function map]

   147   \begin{definition}[Relation map and function map]\\

   159 (* Describe what containers are? *)

   162 (* Say more about containers? *)

   160 

   163 

   161 text {*

   164 text {*

   165 

   166   To define a constant on the lifted type, an aggregate abstraction

   167   function is applied to the raw constant. Below we describe the operation

   168   that generates

   169   an aggregate @{term "Abs"} or @{term "Rep"} function given the

   170   compound raw type and the compound quotient type.

   171   This operation will also be used in translations of theorem statements

   172   and in the lifting procedure.

   173 

   174   The operation is additionally able to descend into types for which

   175   maps are known. Such maps for most common types (list, pair, sum,

   176   option, \ldots) are described in Homeier, and our algorithm uses the

   177   same kind of maps. Given the raw compound type and the quotient compound

   178   type the Rep/Abs algorithm does:

   179 

   180   \begin{itemize}

   181   \item For equal types or free type variables return identity.

   182 

   183   \item For function types recurse, change the Rep/Abs flag to

   184      the opposite one for the domain type and compose the

   185      results with @{term "fun_map"}.

   186 

   187   \item For equal type constructors use the appropriate map function

   188      applied to the results for the arguments.

   189 

   190   \item For unequal type constructors, look in the quotients information

   191     for a quotient type that matches, and instantiate the raw type

   192     appropriately getting back an instantiation environment. We apply

   193     the environment to the arguments and recurse composing it with the

   194     aggregate map function.

   195   \end{itemize}

   196 

   197   The first three points above are identical to the algorithm present in

   198   in Homeier's HOL implementation, below is the definition of @{term fconcat}

   199   that shows the last step:

   200 

   201   @{thm fconcat_def[no_vars]}

   202 

   203   The aggregate @{term Abs} function takes a finite set of finite sets

   204   and applies @{term "map rep_fset"} composed with @{term rep_fset} to

   205   its input, obtaining a list of lists, passes the result to @{term concat}

   206   obtaining a list and applies @{term abs_fset} obtaining the composed

   207   finite set.

   208 *}

   209 

   210 subsection {* Respectfulness *}

   211 

   212 text {*

   213 

   214   A respectfulness lemma for a constant states that the equivalence

   215   class returned by this constant depends only on the equivalence

   216   classes of the arguments applied to the constant. This can be

   217   expressed in terms of an aggregate relation between the constant

   218   and itself, for example the respectfullness for @{term "append"}

   219   can be stated as:

   220 

   221   @{thm append_rsp[no_vars]}

   222 

   223   Which is equivalent to:

   224 

   225   @{thm append_rsp[no_vars,simplified fun_rel_def]}

   226 

   227   Below we show the algorithm for finding the aggregate relation.

   228   This algorithm uses

   229   the relation composition which we define as:

   230 

   166   The first operation that we describe is the generation of

   235   Given an aggregate raw type and quotient type:

   167   aggregate Abs or Rep function for two given compound types.

   168   This operation will be used for the constant defnitions

   169   and for the translation of theorems statements. It relies on

   170   knowing map functions and relation functions for container types.

   171   It follows the following algorithm:

   174   \item For equal types or free type variables return identity.

   238   \item ...

   175 

   176   \item For function types recurse, change the Rep/Abs flag to

   177      the opposite one for the domain type and compose the

   178      results with @{term "fun_map"}.

   179 

   180   \item For equal type constructors use the appropriate map function

   181      applied to the results for the arguments.

   182 

   183   \item For unequal type constructors are unequal, we look in the

   184     quotients information for a raw type quotient type pair that

   185     matches the given types. We apply the environment to the arguments

   186     and recurse composing it with the aggregate map function.

   189 

   241   Aggregate @{term "Rep"} and @{term "Abs"} functions are also

   190 

   242   present in composition quotients. An example composition quotient

   191   Rsp and Prs

   243   theorem that needs to be proved is the one needed to lift theorems

   244   about concat:

   245 

   246   @{thm quotient_compose_list[no_vars]}

   247 

   248   Prs