869 \item First for lifted constants, their definitions are the preservation rules for |
869 \item First for lifted constants, their definitions are the preservation rules for |
870 them. |
870 them. |
871 \item For lambda abstractions lambda preservation establishes |
871 \item For lambda abstractions lambda preservation establishes |
872 the equality between the injected theorem and the goal. This allows both |
872 the equality between the injected theorem and the goal. This allows both |
873 abstraction and quantification over lifted types. |
873 abstraction and quantification over lifted types. |
874 @{thm [display] lambda_prs[no_vars]} |
874 @{thm [display] (concl) lambda_prs[no_vars]} |
875 \item Relations over lifted types are folded with: |
875 \item Relations over lifted types are folded with: |
876 @{thm [display] Quotient_rel_rep[no_vars]} |
876 @{thm [display] (concl) Quotient_rel_rep[no_vars]} |
877 \item User given preservation theorems, that allow using higher level operations |
877 \item User given preservation theorems, that allow using higher level operations |
878 and containers of types being lifted. An example may be |
878 and containers of types being lifted. An example may be |
879 @{thm [display] map_prs(1)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]} |
879 @{thm [display] (concl) map_prs(1)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]} |
880 \end{itemize} |
880 \end{itemize} |
881 |
881 |
882 Preservation of relations and user given constant preservation lemmas *} |
882 *} |
883 |
883 |
884 section {* Examples *} |
884 section {* Examples *} |
885 |
885 |
886 (* Mention why equivalence *) |
886 (* Mention why equivalence *) |
887 |
887 |