src/Doc/Datatypes/Datatypes.thy
changeset 53544 2176a7e40786
parent 53543 c6c8dce7e9ab
child 53552 eed6efba4e3f
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Sep 11 17:17:58 2013 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Wed Sep 11 18:32:43 2013 +0200
     1.3 @@ -336,13 +336,6 @@
     1.4  \begin{itemize}
     1.5  \setlength{\itemsep}{0pt}
     1.6  
     1.7 -\item \relax{Set functions} (or \relax{natural transformations}):
     1.8 -@{text t_set1}, \ldots, @{text t_setm}
     1.9 -
    1.10 -\item \relax{Map function} (or \relax{functorial action}): @{text t_map}
    1.11 -
    1.12 -\item \relax{Relator}: @{text t_rel}
    1.13 -
    1.14  \item \relax{Case combinator}: @{text t_case} (rendered using the familiar
    1.15  @{text case}--@{text of} syntax)
    1.16  
    1.17 @@ -357,6 +350,14 @@
    1.18  @{text t.un_C\<^sub>11}$, \ldots, @{text t.un_C\<^sub>1k\<^sub>1}, \\
    1.19  \phantom{\relax{Selectors:}} \quad\vdots \\
    1.20  \phantom{\relax{Selectors:}} @{text t.un_C\<^sub>n1}$, \ldots, @{text t.un_C\<^sub>nk\<^sub>n}.
    1.21 +
    1.22 +\item \relax{Set functions} (or \relax{natural transformations}):
    1.23 +@{text t_set1}, \ldots, @{text t_setm}
    1.24 +
    1.25 +\item \relax{Map function} (or \relax{functorial action}): @{text t_map}
    1.26 +
    1.27 +\item \relax{Relator}: @{text t_rel}
    1.28 +
    1.29  \end{itemize}
    1.30  
    1.31  \noindent
    1.32 @@ -377,7 +378,7 @@
    1.33        Cons (infixr "#" 65)
    1.34  
    1.35      hide_type list
    1.36 -    hide_const Nil Cons hd tl map
    1.37 +    hide_const Nil Cons hd tl set map list_all2 list_case list_rec
    1.38  
    1.39      locale dummy_list
    1.40      begin
    1.41 @@ -533,26 +534,23 @@
    1.42    \label{ssec:datatype-generated-theorems} *}
    1.43  
    1.44  text {*
    1.45 -The characteristic theorems generated by @{command datatype_new} are
    1.46 -grouped in three broad categories:
    1.47 +The characteristic theorems generated by @{command datatype_new} are grouped in
    1.48 +two broad categories:
    1.49  
    1.50  \begin{itemize}
    1.51  \item The \emph{free constructor theorems} are properties about the constructors
    1.52  and destructors that can be derived for any freely generated type. Internally,
    1.53  the derivation is performed by @{command wrap_free_constructors}.
    1.54  
    1.55 -\item The \emph{per-datatype theorems} are properties connected to individual
    1.56 -datatypes and that rely on their inductive nature.
    1.57 -
    1.58 -\item The \emph{mutual datatype theorems} are properties associated to mutually
    1.59 -recursive groups of datatypes.
    1.60 +\item The \emph{inductive theorems} are properties of datatypes that rely on
    1.61 +their inductive nature.
    1.62  \end{itemize}
    1.63  
    1.64  \noindent
    1.65  The full list of named theorems can be obtained as usual by entering the
    1.66  command \keyw{print\_theorems} immediately after the datatype definition.
    1.67  This list normally excludes low-level theorems that reveal internal
    1.68 -constructions. To see these as well, add the following line to the top of your
    1.69 +constructions. To make these accessible, add the following line to the top of your
    1.70  theory file:
    1.71  *}
    1.72  
    1.73 @@ -573,17 +571,18 @@
    1.74  They are listed below for @{typ "'a list"}:
    1.75  
    1.76  \begin{description}
    1.77 -\item[@{text "t.distinct [simp, induct_simp]"}:] ~ \\
    1.78 +
    1.79 +\item[@{text "t."}\hthm{inject} @{text "[iff, induct_simp]"}:] ~ \\
    1.80 +@{thm list.inject[no_vars]}
    1.81 +
    1.82 +\item[@{text "t."}\hthm{distinct} @{text "[simp, induct_simp]"}:] ~ \\
    1.83  @{thm list.distinct(1)[no_vars]} \\
    1.84  @{thm list.distinct(2)[no_vars]}
    1.85  
    1.86 -\item[@{text "t.inject [iff, induct_simp]"}:] ~ \\
    1.87 -@{thm list.inject[no_vars]}
    1.88 -
    1.89 -\item[@{text "t.exhaust [cases t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}:] ~ \\
    1.90 +\item[@{text "t."}\hthm{exhaust} @{text "[cases t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}:] ~ \\
    1.91  @{thm list.exhaust[no_vars]}
    1.92  
    1.93 -\item[@{text t.nchotomy}:] ~ \\
    1.94 +\item[@{text "t."}\hthm{nchotomy}:] ~ \\
    1.95  @{thm list.nchotomy[no_vars]}
    1.96  
    1.97  \end{description}
    1.98 @@ -592,23 +591,24 @@
    1.99  The next subgroup is concerned with the case combinator:
   1.100  
   1.101  \begin{description}
   1.102 -\item[@{text "t.case [simp]"}:] ~ \\
   1.103 +
   1.104 +\item[@{text "t."}\hthm{case} @{text "[simp]"}:] ~ \\
   1.105  @{thm list.case(1)[no_vars]} \\
   1.106  @{thm list.case(2)[no_vars]}
   1.107  
   1.108 -\item[@{text t.case_cong}:] ~ \\
   1.109 +\item[@{text "t."}\hthm{case\_cong}:] ~ \\
   1.110  @{thm list.case_cong[no_vars]}
   1.111  
   1.112 -\item[@{text "t.weak_case_cong [cong]"}:] ~ \\
   1.113 +\item[@{text "t."}\hthm{weak\_case\_cong} @{text "[cong]"}:] ~ \\
   1.114  @{thm list.weak_case_cong[no_vars]}
   1.115  
   1.116 -\item[@{text t.split}:] ~ \\
   1.117 +\item[@{text "t."}\hthm{split}:] ~ \\
   1.118  @{thm list.split[no_vars]}
   1.119  
   1.120 -\item[@{text t.split_asm}:] ~ \\
   1.121 +\item[@{text "t."}\hthm{split\_asm}:] ~ \\
   1.122  @{thm list.split_asm[no_vars]}
   1.123  
   1.124 -\item[@{text "t.splits = split split_asm"}]
   1.125 +\item[@{text "t."}\hthm{splits} = @{text "split split_asm"}]
   1.126  
   1.127  \end{description}
   1.128  
   1.129 @@ -616,54 +616,88 @@
   1.130  The third and last subgroup revolves around discriminators and selectors:
   1.131  
   1.132  \begin{description}
   1.133 -\item[@{text "discs [simp]"}:] ~ \\
   1.134 +
   1.135 +\item[@{text "t."}\hthm{discs} @{text "[simp]"}:] ~ \\
   1.136  @{thm list.discs(1)[no_vars]} \\
   1.137  @{thm list.discs(2)[no_vars]}
   1.138  
   1.139 -\item[@{text "sels [simp]"}:] ~ \\
   1.140 +\item[@{text "t."}\hthm{sels} @{text "[simp]"}:] ~ \\
   1.141  @{thm list.sels(1)[no_vars]} \\
   1.142  @{thm list.sels(2)[no_vars]}
   1.143  
   1.144 -\item[@{text "collapse [simp]"}:] ~ \\
   1.145 +\item[@{text "t."}\hthm{collapse} @{text "[simp]"}:] ~ \\
   1.146  @{thm list.collapse(1)[no_vars]} \\
   1.147  @{thm list.collapse(2)[no_vars]}
   1.148  
   1.149 -\item[@{text disc_exclude}:] ~ \\
   1.150 +\item[@{text "t."}\hthm{disc\_exclude}:] ~ \\
   1.151  These properties are missing for @{typ "'a list"} because there is only one
   1.152  proper discriminator. Had the datatype been introduced with a second
   1.153 -discriminator (@{const is_Cons}), they would have read thusly: \\
   1.154 +discriminator called @{const is_Cons}, they would have read thusly: \\[\jot]
   1.155  @{prop "null list \<Longrightarrow> \<not> is_Cons list"} \\
   1.156  @{prop "is_Cons list \<Longrightarrow> \<not> null list"}
   1.157  
   1.158 -\item[@{text "disc_exhaust [case_names C\<^sub>1 \<dots> C\<^sub>n]]"}:] ~ \\
   1.159 +\item[@{text "t."}\hthm{disc\_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}:] ~ \\
   1.160  @{thm list.disc_exhaust[no_vars]}
   1.161  
   1.162 -\item[@{text expand}:] ~ \\
   1.163 +\item[@{text "t."}\hthm{expand}:] ~ \\
   1.164  @{thm list.expand[no_vars]}
   1.165  
   1.166 -\item[@{text t.case_conv}:] ~ \\
   1.167 +\item[@{text "t."}\hthm{case\_conv}:] ~ \\
   1.168  @{thm list.case_conv[no_vars]}
   1.169  
   1.170  \end{description}
   1.171 -
   1.172 -  * Section~\label{sec:generating-free-constructor-theorems}
   1.173  *}
   1.174  
   1.175  
   1.176 -subsubsection {* Per-Datatype Theorems *}
   1.177 +subsubsection {* Inductive Theorems *}
   1.178  
   1.179  text {*
   1.180 -    * sets, map, rel
   1.181 -    * induct, fold, rec
   1.182 -    * simps
   1.183 -*}
   1.184 +
   1.185 +\begin{description}
   1.186 +
   1.187 +\item[@{text "t."}\hthm{induct} @{text "[induct t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}:] ~ \\
   1.188 +@{thm list.induct[no_vars]}
   1.189 +
   1.190 +\item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{induct}: @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}:] ~ \\
   1.191 +Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
   1.192 +prove $m$ properties simultaneously.
   1.193  
   1.194 +\item[@{text "t."}\hthm{fold} @{text "[code]"}:] ~ \\
   1.195 +@{thm list.fold(1)[no_vars]} \\
   1.196 +@{thm list.fold(2)[no_vars]}
   1.197 +
   1.198 +\item[@{text "t."}\hthm{rec} @{text "[code]"}:] ~ \\
   1.199 +@{thm list.rec(1)[no_vars]} \\
   1.200 +@{thm list.rec(2)[no_vars]}
   1.201 +
   1.202 +\item[@{text "t."}\hthm{sets}: @{text "[code]"}] ~ \\
   1.203 +@{thm list.sets(1)[no_vars]} \\
   1.204 +@{thm list.sets(2)[no_vars]}
   1.205  
   1.206 -subsubsection {* Mutual Datatype Theorems *}
   1.207 +\item[@{text "t."}\hthm{map}: @{text "[code]"}] ~ \\
   1.208 +@{thm list.map(1)[no_vars]} \\
   1.209 +@{thm list.map(2)[no_vars]}
   1.210 +
   1.211 +\item[@{text "t."}\hthm{rel\_inject} @{text "[code]"}:] ~ \\
   1.212 +@{thm list.rel_inject(1)[no_vars]} \\
   1.213 +@{thm list.rel_inject(2)[no_vars]}
   1.214 +
   1.215 +\item[@{text "t."}\hthm{rel\_distinct} @{text "[code]"}:] ~ \\
   1.216 +@{thm list.rel_distinct(1)[no_vars]} \\
   1.217 +@{thm list.rel_distinct(2)[no_vars]}
   1.218  
   1.219 -text {*
   1.220 -  * multi-type (``common'') theorems
   1.221 -    * induct
   1.222 +\end{description}
   1.223 +
   1.224 +\noindent
   1.225 +For convenience, @{command datatype_new} also provides the following collection:
   1.226 +
   1.227 +\begin{description}
   1.228 +
   1.229 +\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.fold} @{text t.map} @{text t.rel_inject}] ~ \\
   1.230 +@{text t.rel_distinct} @{text t.sets}
   1.231 +
   1.232 +\end{description}
   1.233 +
   1.234  *}
   1.235  
   1.236