245 |
245 |
246 In addition we are able to address the criticism by Paulson \cite{Paulson06} cited |
246 In addition we are able to address the criticism by Paulson \cite{Paulson06} cited |
247 at the beginning of this section about having to collect theorems that are |
247 at the beginning of this section about having to collect theorems that are |
248 lifted from the raw level to the quotient level into one giant list. Our |
248 lifted from the raw level to the quotient level into one giant list. Our |
249 quotient package is the first one that is modular so that it allows to lift |
249 quotient package is the first one that is modular so that it allows to lift |
250 %%% FIXME: First-order ones exist, for example in HOL-Light the lift_theorem function |
250 single higher-order theorems separately. This has the advantage for the user of being able to develop a |
251 %%% takes all the prerequisites and one single theorem to lift. |
|
252 single theorems separately. This has the advantage for the user of being able to develop a |
|
253 formal theory interactively as a natural progression. A pleasing side-result of |
251 formal theory interactively as a natural progression. A pleasing side-result of |
254 the modularity is that we are able to clearly specify what is involved |
252 the modularity is that we are able to clearly specify what is involved |
255 in the lifting process (this was only hinted at in \cite{Homeier05} and |
253 in the lifting process (this was only hinted at in \cite{Homeier05} and |
256 implemented as a ``rough recipe'' in ML-code). |
254 implemented as a ``rough recipe'' in ML-code). |
257 |
255 |
394 \noindent |
392 \noindent |
395 Unfortunately, there are two predicaments with compositions of relations. |
393 Unfortunately, there are two predicaments with compositions of relations. |
396 First, a general quotient theorem, like the one given in Proposition \ref{funquot}, |
394 First, a general quotient theorem, like the one given in Proposition \ref{funquot}, |
397 cannot be stated inside HOL, because of the restriction on types. |
395 cannot be stated inside HOL, because of the restriction on types. |
398 Second, even if we were able to state such a quotient theorem, it |
396 Second, even if we were able to state such a quotient theorem, it |
399 would not be true in general. However, we can prove specific and useful |
397 would not be true in general. However, we can prove specific instances of a |
400 instances of the quotient theorem. We will |
398 quotient theorem for composing particular quotient relations. |
401 show an example in Section \ref{sec:resp}. |
399 To lift @{term flat} the quotient theorem for composing @{text "\<approx>\<^bsub>list\<^esub>"} |
402 %%% FIXME the example is gone from the paper? Maybe we can just put it here? |
400 is necessary: |
|
401 % It says when lists are being quotiented to finite sets, |
|
402 % the contents of the lists can be quotiented as well |
|
403 If @{term R} is an equivalence relation and @{term "Quotient R Abs Rep"} then |
|
404 |
|
405 @{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)"} |
|
406 |
|
407 \vspace{-.5mm} |
|
408 |
403 |
409 |
404 *} |
410 *} |
405 |
411 |
406 section {* Quotient Types and Quotient Definitions\label{sec:type} *} |
412 section {* Quotient Types and Quotient Definitions\label{sec:type} *} |
407 |
413 |