186 |
186 |
187 \item For equal type constructors use the appropriate map function |
187 \item For equal type constructors use the appropriate map function |
188 applied to the results for the arguments. |
188 applied to the results for the arguments. |
189 |
189 |
190 \item For unequal type constructors, look in the quotients information |
190 \item For unequal type constructors, look in the quotients information |
191 for a quotient type that matches, and instantiate the raw type |
191 for a quotient type that matches the type constructor, and instantiate |
|
192 the raw type |
192 appropriately getting back an instantiation environment. We apply |
193 appropriately getting back an instantiation environment. We apply |
193 the environment to the arguments and recurse composing it with the |
194 the environment to the arguments and recurse composing it with the |
194 aggregate map function. |
195 aggregate map function. |
195 \end{itemize} |
196 \end{itemize} |
196 |
197 |
233 \end{definition} |
234 \end{definition} |
234 |
235 |
235 Given an aggregate raw type and quotient type: |
236 Given an aggregate raw type and quotient type: |
236 |
237 |
237 \begin{itemize} |
238 \begin{itemize} |
238 \item ... |
239 \item For equal types or free type variables return equality |
|
240 |
|
241 \item For equal type constructors use the appropriate rel |
|
242 function applied to the results for the argument pairs |
|
243 |
|
244 \item For unequal type constructors, look in the quotients information |
|
245 for a quotient type that matches the type constructor, and instantiate |
|
246 the type appropriately getting back an instantiation environment. We |
|
247 apply the environment to the arguments and recurse composing it with |
|
248 the aggregate relation function. |
|
249 |
239 \end{itemize} |
250 \end{itemize} |
240 |
251 |
|
252 Again, the the behaviour of our algorithm in the last situation is |
|
253 novel, so lets look at the example of respectfullness for @{term concat}: |
|
254 |
|
255 @{thm concat_rsp} |
|
256 |
|
257 This means... |
|
258 |
|
259 *} |
|
260 |
|
261 subsection {* Preservation *} |
|
262 |
|
263 section {* Lifting Theorems *} |
|
264 |
|
265 text{* |
241 Aggregate @{term "Rep"} and @{term "Abs"} functions are also |
266 Aggregate @{term "Rep"} and @{term "Abs"} functions are also |
242 present in composition quotients. An example composition quotient |
267 present in composition quotients. An example composition quotient |
243 theorem that needs to be proved is the one needed to lift theorems |
268 theorem that needs to be proved is the one needed to lift theorems |
244 about concat: |
269 about concat: |
245 |
270 |
246 @{thm quotient_compose_list[no_vars]} |
271 @{thm quotient_compose_list[no_vars]} |
247 |
272 *} |
248 Prs |
|
249 *} |
|
250 |
|
251 section {* Lifting Theorems *} |
|
252 |
273 |
253 text {* TBD *} |
274 text {* TBD *} |
254 |
275 |
255 text {* Why providing a statement to prove is necessary is some cases *} |
276 text {* Why providing a statement to prove is necessary is some cases *} |
256 |
277 |