equal
deleted
inserted
replaced
363 % |
363 % |
364 @{thm [mode=Rule, display, indent=10] pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} |
364 @{thm [mode=Rule, display, indent=10] pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} |
365 \end{definition} |
365 \end{definition} |
366 |
366 |
367 \noindent |
367 \noindent |
368 Unfortunately, restrictions in HOL's type-system prevent us from stating |
368 Unfortunately a quotient type theorem, like Proposition \ref{funquot}, for |
369 and proving a quotient type theorem, like Proposition \ref{funquot}, for compositions |
369 the composition of any two quotients in not true (it is not even typable in |
370 of relations. However, we can prove all instances where @{text R\<^isub>1} and |
370 the HOL type system). However, we can prove useful instances for compatible |
371 @{text "R\<^isub>2"} are built up by constituent equivalence relations. |
371 containers. We will show such example in Section \ref{sec:resp}. |
|
372 |
372 *} |
373 *} |
373 |
374 |
374 section {* Quotient Types and Quotient Definitions\label{sec:type} *} |
375 section {* Quotient Types and Quotient Definitions\label{sec:type} *} |
375 |
376 |
376 text {* |
377 text {* |
726 when we compose the quotient with itself, as there is no simple |
727 when we compose the quotient with itself, as there is no simple |
727 intermediate step. |
728 intermediate step. |
728 |
729 |
729 Lets take again the example of @{term flat}. To be able to lift |
730 Lets take again the example of @{term flat}. To be able to lift |
730 theorems that talk about it we provide the composition quotient |
731 theorems that talk about it we provide the composition quotient |
731 theorem: |
732 theorem which allows quotienting inside the container: |
732 |
733 |
733 @{thm [display, indent=10] quotient_compose_list[no_vars]} |
734 If @{term R} is an equivalence relation and @{term "Quotient R Abs Rep"} |
|
735 then |
|
736 |
|
737 @{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)"} |
734 |
738 |
735 \noindent |
739 \noindent |
736 this theorem will then instantiate the quotients needed in the |
740 this theorem will then instantiate the quotients needed in the |
737 injection and cleaning proofs allowing the lifting procedure to |
741 injection and cleaning proofs allowing the lifting procedure to |
738 proceed in an unchanged way. |
742 proceed in an unchanged way. |