tuned whitespace
authorhaftmann
Fri Aug 27 14:22:33 2010 +0200 (2010-08-27)
changeset 38812e527a34bf69d
parent 38811 c3511b112595
child 38813 f50f0802ba99
tuned whitespace
doc-src/Classes/Thy/Classes.thy
     1.1 --- a/doc-src/Classes/Thy/Classes.thy	Fri Aug 27 14:22:15 2010 +0200
     1.2 +++ b/doc-src/Classes/Thy/Classes.thy	Fri Aug 27 14:22:33 2010 +0200
     1.3 @@ -8,14 +8,14 @@
     1.4    Type classes were introduced by Wadler and Blott \cite{wadler89how}
     1.5    into the Haskell language to allow for a reasonable implementation
     1.6    of overloading\footnote{throughout this tutorial, we are referring
     1.7 -  to classical Haskell 1.0 type classes, not considering
     1.8 -  later additions in expressiveness}.
     1.9 -  As a canonical example, a polymorphic equality function
    1.10 -  @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on different
    1.11 -  types for @{text "\<alpha>"}, which is achieved by splitting introduction
    1.12 -  of the @{text eq} function from its overloaded definitions by means
    1.13 -  of @{text class} and @{text instance} declarations:
    1.14 -  \footnote{syntax here is a kind of isabellized Haskell}
    1.15 +  to classical Haskell 1.0 type classes, not considering later
    1.16 +  additions in expressiveness}.  As a canonical example, a polymorphic
    1.17 +  equality function @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on
    1.18 +  different types for @{text "\<alpha>"}, which is achieved by splitting
    1.19 +  introduction of the @{text eq} function from its overloaded
    1.20 +  definitions by means of @{text class} and @{text instance}
    1.21 +  declarations: \footnote{syntax here is a kind of isabellized
    1.22 +  Haskell}
    1.23  
    1.24    \begin{quote}
    1.25  
    1.26 @@ -41,14 +41,14 @@
    1.27    these annotations are assertions that a particular polymorphic type
    1.28    provides definitions for overloaded functions.
    1.29  
    1.30 -  Indeed, type classes not only allow for simple overloading
    1.31 -  but form a generic calculus, an instance of order-sorted
    1.32 -  algebra \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
    1.33 +  Indeed, type classes not only allow for simple overloading but form
    1.34 +  a generic calculus, an instance of order-sorted algebra
    1.35 +  \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
    1.36  
    1.37 -  From a software engineering point of view, type classes
    1.38 -  roughly correspond to interfaces in object-oriented languages like Java;
    1.39 -  so, it is naturally desirable that type classes do not only
    1.40 -  provide functions (class parameters) but also state specifications
    1.41 +  From a software engineering point of view, type classes roughly
    1.42 +  correspond to interfaces in object-oriented languages like Java; so,
    1.43 +  it is naturally desirable that type classes do not only provide
    1.44 +  functions (class parameters) but also state specifications
    1.45    implementations must obey.  For example, the @{text "class eq"}
    1.46    above could be given the following specification, demanding that
    1.47    @{text "class eq"} is an equivalence relation obeying reflexivity,
    1.48 @@ -65,11 +65,10 @@
    1.49  
    1.50    \end{quote}
    1.51  
    1.52 -  \noindent From a theoretical point of view, type classes are lightweight
    1.53 -  modules; Haskell type classes may be emulated by
    1.54 -  SML functors \cite{classes_modules}. 
    1.55 -  Isabelle/Isar offers a discipline of type classes which brings
    1.56 -  all those aspects together:
    1.57 +  \noindent From a theoretical point of view, type classes are
    1.58 +  lightweight modules; Haskell type classes may be emulated by SML
    1.59 +  functors \cite{classes_modules}.  Isabelle/Isar offers a discipline
    1.60 +  of type classes which brings all those aspects together:
    1.61  
    1.62    \begin{enumerate}
    1.63      \item specifying abstract parameters together with
    1.64 @@ -81,15 +80,15 @@
    1.65        locales \cite{kammueller-locales}.
    1.66    \end{enumerate}
    1.67  
    1.68 -  \noindent Isar type classes also directly support code generation
    1.69 -  in a Haskell like fashion. Internally, they are mapped to more primitive 
    1.70 -  Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
    1.71 +  \noindent Isar type classes also directly support code generation in
    1.72 +  a Haskell like fashion. Internally, they are mapped to more
    1.73 +  primitive Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
    1.74  
    1.75 -  This tutorial demonstrates common elements of structured specifications
    1.76 -  and abstract reasoning with type classes by the algebraic hierarchy of
    1.77 -  semigroups, monoids and groups.  Our background theory is that of
    1.78 -  Isabelle/HOL \cite{isa-tutorial}, for which some
    1.79 -  familiarity is assumed.
    1.80 +  This tutorial demonstrates common elements of structured
    1.81 +  specifications and abstract reasoning with type classes by the
    1.82 +  algebraic hierarchy of semigroups, monoids and groups.  Our
    1.83 +  background theory is that of Isabelle/HOL \cite{isa-tutorial}, for
    1.84 +  which some familiarity is assumed.
    1.85  *}
    1.86  
    1.87  section {* A simple algebra example \label{sec:example} *}
    1.88 @@ -107,25 +106,24 @@
    1.89    assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    1.90  
    1.91  text {*
    1.92 -  \noindent This @{command class} specification consists of two
    1.93 -  parts: the \qn{operational} part names the class parameter
    1.94 -  (@{element "fixes"}), the \qn{logical} part specifies properties on them
    1.95 -  (@{element "assumes"}).  The local @{element "fixes"} and
    1.96 -  @{element "assumes"} are lifted to the theory toplevel,
    1.97 -  yielding the global
    1.98 +  \noindent This @{command class} specification consists of two parts:
    1.99 +  the \qn{operational} part names the class parameter (@{element
   1.100 +  "fixes"}), the \qn{logical} part specifies properties on them
   1.101 +  (@{element "assumes"}).  The local @{element "fixes"} and @{element
   1.102 +  "assumes"} are lifted to the theory toplevel, yielding the global
   1.103    parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
   1.104 -  global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y
   1.105 -  z \<Colon> \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
   1.106 +  global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y z \<Colon>
   1.107 +  \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
   1.108  *}
   1.109  
   1.110  
   1.111  subsection {* Class instantiation \label{sec:class_inst} *}
   1.112  
   1.113  text {*
   1.114 -  The concrete type @{typ int} is made a @{class semigroup}
   1.115 -  instance by providing a suitable definition for the class parameter
   1.116 -  @{text "(\<otimes>)"} and a proof for the specification of @{fact assoc}.
   1.117 -  This is accomplished by the @{command instantiation} target:
   1.118 +  The concrete type @{typ int} is made a @{class semigroup} instance
   1.119 +  by providing a suitable definition for the class parameter @{text
   1.120 +  "(\<otimes>)"} and a proof for the specification of @{fact assoc}.  This is
   1.121 +  accomplished by the @{command instantiation} target:
   1.122  *}
   1.123  
   1.124  instantiation %quote int :: semigroup
   1.125 @@ -143,22 +141,22 @@
   1.126  end %quote
   1.127  
   1.128  text {*
   1.129 -  \noindent @{command instantiation} defines class parameters
   1.130 -  at a particular instance using common specification tools (here,
   1.131 -  @{command definition}).  The concluding @{command instance}
   1.132 -  opens a proof that the given parameters actually conform
   1.133 -  to the class specification.  Note that the first proof step
   1.134 -  is the @{method default} method,
   1.135 -  which for such instance proofs maps to the @{method intro_classes} method.
   1.136 -  This reduces an instance judgement to the relevant primitive
   1.137 -  proof goals; typically it is the first method applied
   1.138 -  in an instantiation proof.
   1.139 +  \noindent @{command instantiation} defines class parameters at a
   1.140 +  particular instance using common specification tools (here,
   1.141 +  @{command definition}).  The concluding @{command instance} opens a
   1.142 +  proof that the given parameters actually conform to the class
   1.143 +  specification.  Note that the first proof step is the @{method
   1.144 +  default} method, which for such instance proofs maps to the @{method
   1.145 +  intro_classes} method.  This reduces an instance judgement to the
   1.146 +  relevant primitive proof goals; typically it is the first method
   1.147 +  applied in an instantiation proof.
   1.148  
   1.149 -  From now on, the type-checker will consider @{typ int}
   1.150 -  as a @{class semigroup} automatically, i.e.\ any general results
   1.151 -  are immediately available on concrete instances.
   1.152 +  From now on, the type-checker will consider @{typ int} as a @{class
   1.153 +  semigroup} automatically, i.e.\ any general results are immediately
   1.154 +  available on concrete instances.
   1.155  
   1.156 -  \medskip Another instance of @{class semigroup} yields the natural numbers:
   1.157 +  \medskip Another instance of @{class semigroup} yields the natural
   1.158 +  numbers:
   1.159  *}
   1.160  
   1.161  instantiation %quote nat :: semigroup
   1.162 @@ -177,21 +175,20 @@
   1.163  end %quote
   1.164  
   1.165  text {*
   1.166 -  \noindent Note the occurence of the name @{text mult_nat}
   1.167 -  in the primrec declaration;  by default, the local name of
   1.168 -  a class operation @{text f} to be instantiated on type constructor
   1.169 -  @{text \<kappa>} is mangled as @{text f_\<kappa>}.  In case of uncertainty,
   1.170 -  these names may be inspected using the @{command "print_context"} command
   1.171 -  or the corresponding ProofGeneral button.
   1.172 +  \noindent Note the occurence of the name @{text mult_nat} in the
   1.173 +  primrec declaration; by default, the local name of a class operation
   1.174 +  @{text f} to be instantiated on type constructor @{text \<kappa>} is
   1.175 +  mangled as @{text f_\<kappa>}.  In case of uncertainty, these names may be
   1.176 +  inspected using the @{command "print_context"} command or the
   1.177 +  corresponding ProofGeneral button.
   1.178  *}
   1.179  
   1.180  subsection {* Lifting and parametric types *}
   1.181  
   1.182  text {*
   1.183 -  Overloaded definitions given at a class instantiation
   1.184 -  may include recursion over the syntactic structure of types.
   1.185 -  As a canonical example, we model product semigroups
   1.186 -  using our simple algebra:
   1.187 +  Overloaded definitions given at a class instantiation may include
   1.188 +  recursion over the syntactic structure of types.  As a canonical
   1.189 +  example, we model product semigroups using our simple algebra:
   1.190  *}
   1.191  
   1.192  instantiation %quote prod :: (semigroup, semigroup) semigroup
   1.193 @@ -211,21 +208,19 @@
   1.194  text {*
   1.195    \noindent Associativity of product semigroups is established using
   1.196    the definition of @{text "(\<otimes>)"} on products and the hypothetical
   1.197 -  associativity of the type components;  these hypotheses
   1.198 -  are legitimate due to the @{class semigroup} constraints imposed
   1.199 -  on the type components by the @{command instance} proposition.
   1.200 -  Indeed, this pattern often occurs with parametric types
   1.201 -  and type classes.
   1.202 +  associativity of the type components; these hypotheses are
   1.203 +  legitimate due to the @{class semigroup} constraints imposed on the
   1.204 +  type components by the @{command instance} proposition.  Indeed,
   1.205 +  this pattern often occurs with parametric types and type classes.
   1.206  *}
   1.207  
   1.208  
   1.209  subsection {* Subclassing *}
   1.210  
   1.211  text {*
   1.212 -  We define a subclass @{text monoidl} (a semigroup with a left-hand neutral)
   1.213 -  by extending @{class semigroup}
   1.214 -  with one additional parameter @{text neutral} together
   1.215 -  with its characteristic property:
   1.216 +  We define a subclass @{text monoidl} (a semigroup with a left-hand
   1.217 +  neutral) by extending @{class semigroup} with one additional
   1.218 +  parameter @{text neutral} together with its characteristic property:
   1.219  *}
   1.220  
   1.221  class %quote monoidl = semigroup +
   1.222 @@ -233,10 +228,10 @@
   1.223    assumes neutl: "\<one> \<otimes> x = x"
   1.224  
   1.225  text {*
   1.226 -  \noindent Again, we prove some instances, by
   1.227 -  providing suitable parameter definitions and proofs for the
   1.228 -  additional specifications.  Observe that instantiations
   1.229 -  for types with the same arity may be simultaneous:
   1.230 +  \noindent Again, we prove some instances, by providing suitable
   1.231 +  parameter definitions and proofs for the additional specifications.
   1.232 +  Observe that instantiations for types with the same arity may be
   1.233 +  simultaneous:
   1.234  *}
   1.235  
   1.236  instantiation %quote nat and int :: monoidl
   1.237 @@ -309,8 +304,8 @@
   1.238  end %quote
   1.239  
   1.240  text {*
   1.241 -  \noindent To finish our small algebra example, we add a @{text group} class
   1.242 -  with a corresponding instance:
   1.243 +  \noindent To finish our small algebra example, we add a @{text
   1.244 +  group} class with a corresponding instance:
   1.245  *}
   1.246  
   1.247  class %quote group = monoidl +
   1.248 @@ -338,9 +333,9 @@
   1.249  subsection {* A look behind the scenes *}
   1.250  
   1.251  text {*
   1.252 -  The example above gives an impression how Isar type classes work
   1.253 -  in practice.  As stated in the introduction, classes also provide
   1.254 -  a link to Isar's locale system.  Indeed, the logical core of a class
   1.255 +  The example above gives an impression how Isar type classes work in
   1.256 +  practice.  As stated in the introduction, classes also provide a
   1.257 +  link to Isar's locale system.  Indeed, the logical core of a class
   1.258    is nothing other than a locale:
   1.259  *}
   1.260  
   1.261 @@ -402,13 +397,14 @@
   1.262  qed
   1.263  
   1.264  text {*
   1.265 -  \noindent Here the \qt{@{keyword "in"} @{class group}} target specification
   1.266 -  indicates that the result is recorded within that context for later
   1.267 -  use.  This local theorem is also lifted to the global one @{fact
   1.268 -  "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon> \<alpha>\<Colon>group. x \<otimes> y = x \<otimes>
   1.269 -  z \<longleftrightarrow> y = z"}.  Since type @{text "int"} has been made an instance of
   1.270 -  @{text "group"} before, we may refer to that fact as well: @{prop
   1.271 -  [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.
   1.272 +  \noindent Here the \qt{@{keyword "in"} @{class group}} target
   1.273 +  specification indicates that the result is recorded within that
   1.274 +  context for later use.  This local theorem is also lifted to the
   1.275 +  global one @{fact "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon>
   1.276 +  \<alpha>\<Colon>group. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.  Since type @{text "int"} has been
   1.277 +  made an instance of @{text "group"} before, we may refer to that
   1.278 +  fact as well: @{prop [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y =
   1.279 +  z"}.
   1.280  *}
   1.281  
   1.282  
   1.283 @@ -424,15 +420,14 @@
   1.284  
   1.285  text {*
   1.286    \noindent If the locale @{text group} is also a class, this local
   1.287 -  definition is propagated onto a global definition of
   1.288 -  @{term [source] "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"}
   1.289 -  with corresponding theorems
   1.290 +  definition is propagated onto a global definition of @{term [source]
   1.291 +  "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"} with corresponding theorems
   1.292  
   1.293    @{thm pow_nat.simps [no_vars]}.
   1.294  
   1.295 -  \noindent As you can see from this example, for local
   1.296 -  definitions you may use any specification tool
   1.297 -  which works together with locales, such as Krauss's recursive function package
   1.298 +  \noindent As you can see from this example, for local definitions
   1.299 +  you may use any specification tool which works together with
   1.300 +  locales, such as Krauss's recursive function package
   1.301    \cite{krauss2006}.
   1.302  *}
   1.303  
   1.304 @@ -440,19 +435,17 @@
   1.305  subsection {* A functor analogy *}
   1.306  
   1.307  text {*
   1.308 -  We introduced Isar classes by analogy to type classes in
   1.309 -  functional programming;  if we reconsider this in the
   1.310 -  context of what has been said about type classes and locales,
   1.311 -  we can drive this analogy further by stating that type
   1.312 -  classes essentially correspond to functors that have
   1.313 -  a canonical interpretation as type classes.
   1.314 -  There is also the possibility of other interpretations.
   1.315 -  For example, @{text list}s also form a monoid with
   1.316 -  @{text append} and @{term "[]"} as operations, but it
   1.317 -  seems inappropriate to apply to lists
   1.318 -  the same operations as for genuinely algebraic types.
   1.319 -  In such a case, we can simply make a particular interpretation
   1.320 -  of monoids for lists:
   1.321 +  We introduced Isar classes by analogy to type classes in functional
   1.322 +  programming; if we reconsider this in the context of what has been
   1.323 +  said about type classes and locales, we can drive this analogy
   1.324 +  further by stating that type classes essentially correspond to
   1.325 +  functors that have a canonical interpretation as type classes.
   1.326 +  There is also the possibility of other interpretations.  For
   1.327 +  example, @{text list}s also form a monoid with @{text append} and
   1.328 +  @{term "[]"} as operations, but it seems inappropriate to apply to
   1.329 +  lists the same operations as for genuinely algebraic types.  In such
   1.330 +  a case, we can simply make a particular interpretation of monoids
   1.331 +  for lists:
   1.332  *}
   1.333  
   1.334  interpretation %quote list_monoid: monoid append "[]"
   1.335 @@ -510,12 +503,10 @@
   1.336  qed
   1.337  
   1.338  text {*
   1.339 -  The logical proof is carried out on the locale level.
   1.340 -  Afterwards it is propagated
   1.341 -  to the type system, making @{text group} an instance of
   1.342 -  @{text monoid} by adding an additional edge
   1.343 -  to the graph of subclass relations
   1.344 -  (\figref{fig:subclass}).
   1.345 +  The logical proof is carried out on the locale level.  Afterwards it
   1.346 +  is propagated to the type system, making @{text group} an instance
   1.347 +  of @{text monoid} by adding an additional edge to the graph of
   1.348 +  subclass relations (\figref{fig:subclass}).
   1.349  
   1.350    \begin{figure}[htbp]
   1.351     \begin{center}
   1.352 @@ -547,8 +538,8 @@
   1.353     \end{center}
   1.354    \end{figure}
   1.355  
   1.356 -  For illustration, a derived definition
   1.357 -  in @{text group} using @{text pow_nat}
   1.358 +  For illustration, a derived definition in @{text group} using @{text
   1.359 +  pow_nat}
   1.360  *}
   1.361  
   1.362  definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
   1.363 @@ -557,17 +548,17 @@
   1.364      else (pow_nat (nat (- k)) x)\<div>)"
   1.365  
   1.366  text {*
   1.367 -  \noindent yields the global definition of
   1.368 -  @{term [source] "pow_int \<Colon> int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"}
   1.369 -  with the corresponding theorem @{thm pow_int_def [no_vars]}.
   1.370 +  \noindent yields the global definition of @{term [source] "pow_int \<Colon>
   1.371 +  int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"} with the corresponding theorem @{thm
   1.372 +  pow_int_def [no_vars]}.
   1.373  *}
   1.374  
   1.375  subsection {* A note on syntax *}
   1.376  
   1.377  text {*
   1.378 -  As a convenience, class context syntax allows references
   1.379 -  to local class operations and their global counterparts
   1.380 -  uniformly;  type inference resolves ambiguities.  For example:
   1.381 +  As a convenience, class context syntax allows references to local
   1.382 +  class operations and their global counterparts uniformly; type
   1.383 +  inference resolves ambiguities.  For example:
   1.384  *}
   1.385  
   1.386  context %quote semigroup
   1.387 @@ -581,11 +572,11 @@
   1.388  term %quote "x \<otimes> y" -- {* example 3 *}
   1.389  
   1.390  text {*
   1.391 -  \noindent Here in example 1, the term refers to the local class operation
   1.392 -  @{text "mult [\<alpha>]"}, whereas in example 2 the type constraint
   1.393 -  enforces the global class operation @{text "mult [nat]"}.
   1.394 -  In the global context in example 3, the reference is
   1.395 -  to the polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
   1.396 +  \noindent Here in example 1, the term refers to the local class
   1.397 +  operation @{text "mult [\<alpha>]"}, whereas in example 2 the type
   1.398 +  constraint enforces the global class operation @{text "mult [nat]"}.
   1.399 +  In the global context in example 3, the reference is to the
   1.400 +  polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
   1.401  *}
   1.402  
   1.403  section {* Further issues *}
   1.404 @@ -593,16 +584,14 @@
   1.405  subsection {* Type classes and code generation *}
   1.406  
   1.407  text {*
   1.408 -  Turning back to the first motivation for type classes,
   1.409 -  namely overloading, it is obvious that overloading
   1.410 -  stemming from @{command class} statements and
   1.411 -  @{command instantiation}
   1.412 -  targets naturally maps to Haskell type classes.
   1.413 -  The code generator framework \cite{isabelle-codegen} 
   1.414 -  takes this into account.  If the target language (e.g.~SML)
   1.415 -  lacks type classes, then they
   1.416 -  are implemented by an explicit dictionary construction.
   1.417 -  As example, let's go back to the power function:
   1.418 +  Turning back to the first motivation for type classes, namely
   1.419 +  overloading, it is obvious that overloading stemming from @{command
   1.420 +  class} statements and @{command instantiation} targets naturally
   1.421 +  maps to Haskell type classes.  The code generator framework
   1.422 +  \cite{isabelle-codegen} takes this into account.  If the target
   1.423 +  language (e.g.~SML) lacks type classes, then they are implemented by
   1.424 +  an explicit dictionary construction.  As example, let's go back to
   1.425 +  the power function:
   1.426  *}
   1.427  
   1.428  definition %quote example :: int where
   1.429 @@ -619,11 +608,18 @@
   1.430  *}
   1.431  text %quote {*@{code_stmts example (SML)}*}
   1.432  
   1.433 +text {*
   1.434 +  \noindent In Scala, implicts are used as dictionaries:
   1.435 +*}
   1.436 +(*<*)code_include %invisible Scala "Natural" -(*>*)
   1.437 +text %quote {*@{code_stmts example (Scala)}*}
   1.438 +
   1.439 +
   1.440  subsection {* Inspecting the type class universe *}
   1.441  
   1.442  text {*
   1.443 -  To facilitate orientation in complex subclass structures,
   1.444 -  two diagnostics commands are provided:
   1.445 +  To facilitate orientation in complex subclass structures, two
   1.446 +  diagnostics commands are provided:
   1.447  
   1.448    \begin{description}
   1.449