396 |
396 |
397 \begin{definition}[Composition of Relations] |
397 \begin{definition}[Composition of Relations] |
398 @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate |
398 @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate |
399 composition defined by |
399 composition defined by |
400 @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} |
400 @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} |
401 holds if and only if @{thm (prem 1) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} and |
401 holds if and only if there exists a @{text y} such that @{thm (prem 1) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} and |
402 @{thm (prem 2) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}. |
402 @{thm (prem 2) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}. |
403 \end{definition} |
403 \end{definition} |
404 |
404 |
405 \noindent |
405 \noindent |
406 Unfortunately, there are two predicaments with compositions of relations. |
406 Unfortunately, there are two predicaments with compositions of relations. |
407 First, a general quotient theorem, like the one given in Proposition \ref{funquot}, |
407 First, a general quotient theorem for @{text "\<circ>\<circ>\<circ>"}, like the one for @{text "\<singlearr>"} |
|
408 given in Proposition \ref{funquot}, |
408 cannot be stated inside HOL, because of restrictions on types. |
409 cannot be stated inside HOL, because of restrictions on types. |
409 Second, even if we were able to state such a quotient theorem, it |
410 Second, even if we were able to state such a quotient theorem, it |
410 would not be true in general. However, we can prove specific instances of a |
411 would not be true in general. However, we can prove specific instances of a |
411 quotient theorem for composing particular quotient relations. |
412 quotient theorem for composing particular quotient relations. |
412 For example, to lift theorems involving @{term flat} the quotient theorem for |
413 For example, to lift theorems involving @{term flat} the quotient theorem for |
567 @{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>as. MAP'(\<sigma>)"} |
568 @{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>as. MAP'(\<sigma>)"} |
568 \end{tabular} |
569 \end{tabular} |
569 \end{center} |
570 \end{center} |
570 % |
571 % |
571 \noindent |
572 \noindent |
572 In this definition we rely on the fact that we can interpret type-variables @{text \<alpha>} as |
573 In this definition we rely on the fact that in the first clause we can interpret type-variables @{text \<alpha>} as |
573 term variables @{text a}. In the last clause we build an abstraction over all |
574 term variables @{text a}. In the last clause we build an abstraction over all |
574 term-variables of the map-function generated by the auxiliary function |
575 term-variables of the map-function generated by the auxiliary function |
575 @{text "MAP'"}. |
576 @{text "MAP'"}. |
576 The need for aggregate map-functions can be seen in cases where we build quotients, |
577 The need for aggregate map-functions can be seen in cases where we build quotients, |
577 say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}. |
578 say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}. |
644 "MAP (\<rho>s \<kappa>)"}, after applying the functions @{text "ABS (\<sigma>s', \<tau>s)"} to it, |
645 "MAP (\<rho>s \<kappa>)"}, after applying the functions @{text "ABS (\<sigma>s', \<tau>s)"} to it, |
645 returns a term of type @{text "\<rho>s[\<sigma>s'] \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}. This type is |
646 returns a term of type @{text "\<rho>s[\<sigma>s'] \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}. This type is |
646 equivalent to @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}, which we just have to compose with |
647 equivalent to @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}, which we just have to compose with |
647 @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"} according to the type of @{text "\<circ>"}.\qed |
648 @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"} according to the type of @{text "\<circ>"}.\qed |
648 \end{proof} |
649 \end{proof} |
649 |
|
650 \noindent |
|
651 The reader should note that this lemma fails for the abstraction and representation |
|
652 functions used in Homeier's quotient package. |
|
653 *} |
650 *} |
654 |
651 |
655 section {* Respectfulness and Preservation \label{sec:resp} *} |
652 section {* Respectfulness and Preservation \label{sec:resp} *} |
656 |
653 |
657 text {* |
654 text {* |