824 |
825 |
825 subsubsection {* Functorial Theorems |
826 subsubsection {* Functorial Theorems |
826 \label{sssec:functorial-theorems} *} |
827 \label{sssec:functorial-theorems} *} |
827 |
828 |
828 text {* |
829 text {* |
829 The BNF-related theorem are as follows: |
830 The functorial theorems are partitioned in two subgroups. The first subgroup |
|
831 consists of properties involving the constructors and either a set function, the |
|
832 map function, or the relator: |
830 |
833 |
831 \begin{indentblock} |
834 \begin{indentblock} |
832 \begin{description} |
835 \begin{description} |
833 |
836 |
834 \item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\ |
837 \item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\ |
851 \end{indentblock} |
854 \end{indentblock} |
852 |
855 |
853 \noindent |
856 \noindent |
854 In addition, equational versions of @{text t.rel_inject} and @{text |
857 In addition, equational versions of @{text t.rel_inject} and @{text |
855 rel_distinct} are registered with the @{text "[code]"} attribute. |
858 rel_distinct} are registered with the @{text "[code]"} attribute. |
|
859 |
|
860 The second subgroup consists of more abstract properties of the set functions, |
|
861 the map function, and the relator: |
|
862 |
|
863 \begin{indentblock} |
|
864 \begin{description} |
|
865 |
|
866 \item[@{text "t."}\hthm{map\_comp}\rm:] ~ \\ |
|
867 @{thm list.map_cong0[no_vars]} |
|
868 |
|
869 \item[@{text "t."}\hthm{map\_cong} @{text "[cong, fundef_cong]"}\rm:] ~ \\ |
|
870 @{thm list.map_cong[no_vars]} |
|
871 |
|
872 \item[@{text "t."}\hthm{map\_id}\rm:] ~ \\ |
|
873 @{thm list.map_id[no_vars]} |
|
874 |
|
875 \item[@{text "t."}\hthm{rel\_compp}\rm:] ~ \\ |
|
876 @{thm list.rel_compp[no_vars]} |
|
877 |
|
878 \item[@{text "t."}\hthm{rel\_conversep}\rm:] ~ \\ |
|
879 @{thm list.rel_conversep[no_vars]} |
|
880 |
|
881 \item[@{text "t."}\hthm{rel\_eq}\rm:] ~ \\ |
|
882 @{thm list.rel_eq[no_vars]} |
|
883 |
|
884 \item[@{text "t."}\hthm{rel\_flip}\rm:] ~ \\ |
|
885 @{thm list.rel_flip[no_vars]} |
|
886 |
|
887 \item[@{text "t."}\hthm{rel\_mono}\rm:] ~ \\ |
|
888 @{thm list.rel_mono[no_vars]} |
|
889 |
|
890 \item[@{text "t."}\hthm{set\_map}\rm:] ~ \\ |
|
891 @{thm list.set_map[no_vars]} |
|
892 |
|
893 \end{description} |
|
894 \end{indentblock} |
856 *} |
895 *} |
857 |
896 |
858 |
897 |
859 subsubsection {* Inductive Theorems |
898 subsubsection {* Inductive Theorems |
860 \label{sssec:inductive-theorems} *} |
899 \label{sssec:inductive-theorems} *} |