equal
deleted
inserted
replaced
833 \end{itemize} |
833 \end{itemize} |
834 |
834 |
835 Otherwise the two terms are applications. There are two cases: If there is a REP/ABS |
835 Otherwise the two terms are applications. There are two cases: If there is a REP/ABS |
836 in the injected theorem we can use the theorem: |
836 in the injected theorem we can use the theorem: |
837 |
837 |
838 @{thm [display] rep_abs_rsp[no_vars]} |
838 @{thm [display, indent=10] rep_abs_rsp[no_vars]} |
839 |
839 |
|
840 \noindent |
840 and continue the proof. |
841 and continue the proof. |
841 |
842 |
842 Otherwise we introduce an appropriate relation between the subterms and continue with |
843 Otherwise we introduce an appropriate relation between the subterms and continue with |
843 two subgoals using the lemma: |
844 two subgoals using the lemma: |
844 |
845 |
845 @{thm [display] apply_rsp[no_vars]} |
846 @{thm [display, indent=10] apply_rsp[no_vars]} |
846 |
847 |
847 *} |
848 *} |
848 |
849 |
849 subsection {* Cleaning *} |
850 subsection {* Cleaning *} |
850 |
851 |
862 @{thm [display] lambda_prs[no_vars]} |
863 @{thm [display] lambda_prs[no_vars]} |
863 \item Relations over lifted types are folded with: |
864 \item Relations over lifted types are folded with: |
864 @{thm [display] Quotient_rel_rep[no_vars]} |
865 @{thm [display] Quotient_rel_rep[no_vars]} |
865 \item User given preservation theorems, that allow using higher level operations |
866 \item User given preservation theorems, that allow using higher level operations |
866 and containers of types being lifted. An example may be |
867 and containers of types being lifted. An example may be |
867 @{thm [display] map_prs(1)[no_vars]} |
868 @{thm [display] map_prs(1)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]} |
868 \end{itemize} |
869 \end{itemize} |
869 |
870 |
870 Preservation of relations and user given constant preservation lemmas *} |
871 Preservation of relations and user given constant preservation lemmas *} |
871 |
872 |
872 section {* Examples *} |
873 section {* Examples *} |
949 |
950 |
950 text {* |
951 text {* |
951 \begin{itemize} |
952 \begin{itemize} |
952 |
953 |
953 \item Peter Homeier's package~\cite{Homeier05} (and related work from there) |
954 \item Peter Homeier's package~\cite{Homeier05} (and related work from there) |
|
955 |
954 \item John Harrison's one~\cite{harrison-thesis} is the first one to lift theorems |
956 \item John Harrison's one~\cite{harrison-thesis} is the first one to lift theorems |
955 but only first order. |
957 but only first order. |
956 |
958 |
957 \item PVS~\cite{PVS:Interpretations} |
959 \item PVS~\cite{PVS:Interpretations} |
958 \item MetaPRL~\cite{Nogin02} |
960 \item MetaPRL~\cite{Nogin02} |
959 \item Manually defined quotients in Isabelle/HOL Library (Markus's Quotient\_Type, |
961 |
960 Dixon's FSet, \ldots) |
962 % \item Manually defined quotients in Isabelle/HOL Library (Markus's Quotient\_Type, |
|
963 % Dixon's FSet, \ldots) |
961 |
964 |
962 \item Oscar Slotosch defines quotient-type automatically but no |
965 \item Oscar Slotosch defines quotient-type automatically but no |
963 lifting~\cite{Slotosch97}. |
966 lifting~\cite{Slotosch97}. |
964 |
967 |
965 \item PER. And how to avoid it. |
968 \item PER. And how to avoid it. |