document property 'disc_map_iff'
authordesharna
Mon May 19 11:27:02 2014 +0200 (2014-05-19)
changeset 56992d0e5225601d3
parent 56991 8e9ca31e9b8e
child 56993 e5366291d6aa
document property 'disc_map_iff'
src/Doc/Datatypes/Datatypes.thy
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Thu May 15 16:15:44 2014 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon May 19 11:27:02 2014 +0200
     1.3 @@ -843,8 +843,8 @@
     1.4  
     1.5  text {*
     1.6  The functorial theorems are partitioned in two subgroups. The first subgroup
     1.7 -consists of properties involving the constructors and either a set function, the
     1.8 -map function, or the relator:
     1.9 +consists of properties involving the constructors or the destructors and either
    1.10 +a set function, the map function, or the relator:
    1.11  
    1.12  \begin{indentblock}
    1.13  \begin{description}
    1.14 @@ -853,10 +853,16 @@
    1.15  @{thm list.set(1)[no_vars]} \\
    1.16  @{thm list.set(2)[no_vars]}
    1.17  
    1.18 +\item[@{text "t."}\hthm{set\_empty}\rm:] ~ \\
    1.19 +@{thm list.set_empty[no_vars]}
    1.20 +
    1.21  \item[@{text "t."}\hthm{map} @{text "[simp, code]"}\rm:] ~ \\
    1.22  @{thm list.map(1)[no_vars]} \\
    1.23  @{thm list.map(2)[no_vars]}
    1.24  
    1.25 +\item[@{text "t."}\hthm{disc\_map\_iff} @{text "[simp]"}\rm:] ~ \\
    1.26 +@{thm list.disc_map_iff[no_vars]}
    1.27 +
    1.28  \item[@{text "t."}\hthm{rel\_inject} @{text "[simp]"}\rm:] ~ \\
    1.29  @{thm list.rel_inject(1)[no_vars]} \\
    1.30  @{thm list.rel_inject(2)[no_vars]}
    1.31 @@ -878,6 +884,9 @@
    1.32  \begin{indentblock}
    1.33  \begin{description}
    1.34  
    1.35 +\item[@{text "t."}\hthm{set\_map}\rm:] ~ \\
    1.36 +@{thm list.set_map[no_vars]}
    1.37 +
    1.38  \item[@{text "t."}\hthm{map\_comp}\rm:] ~ \\
    1.39  @{thm list.map_cong0[no_vars]}
    1.40  
    1.41 @@ -908,12 +917,6 @@
    1.42  \item[@{text "t."}\hthm{rel\_mono}\rm:] ~ \\
    1.43  @{thm list.rel_mono[no_vars]}
    1.44  
    1.45 -\item[@{text "t."}\hthm{set\_empty}\rm:] ~ \\
    1.46 -@{thm list.set_empty[no_vars]}
    1.47 -
    1.48 -\item[@{text "t."}\hthm{set\_map}\rm:] ~ \\
    1.49 -@{thm list.set_map[no_vars]}
    1.50 -
    1.51  \end{description}
    1.52  \end{indentblock}
    1.53  *}