7 chapter {* Isabelle/HOLCF \label{ch:holcf} *}
9 section {* Mixfix syntax for continuous operations *}
12 \begin{matharray}{rcl}
13 @{command_def (HOLCF) "consts"} & : & @{text "theory \<rightarrow> theory"} \\
16 HOLCF provides a separate type for continuous functions @{text "\<alpha> \<rightarrow>
17 \<beta>"}, with an explicit application operator @{term "f \<cdot> x"}.
18 Isabelle mixfix syntax normally refers directly to the pure
19 meta-level function type @{text "\<alpha> \<Rightarrow> \<beta>"}, with application @{text "f
22 The HOLCF variant of @{command (HOLCF) "consts"} modifies that of
23 Pure Isabelle (cf.\ \secref{sec:consts}) such that declarations
24 involving continuous function types are treated specifically. Any
25 given syntax template is transformed internally, generating
26 translation rules for the abstract and concrete representation of
27 continuous application. Note that mixing of HOLCF and Pure
28 application is \emph{not} supported!
32 section {* Recursive domains *}
35 \begin{matharray}{rcl}
36 @{command_def (HOLCF) "domain"} & : & @{text "theory \<rightarrow> theory"} \\
40 'domain' parname? (dmspec + 'and')
43 dmspec: typespec '=' (cons + '|')
45 cons: name (type *) mixfix?
47 dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
50 Recursive domains in HOLCF are analogous to datatypes in classical
51 HOL (cf.\ \secref{sec:hol-datatype}). Mutual recursion is
52 supported, but no nesting nor arbitrary branching. Domain
53 constructors may be strict (default) or lazy, the latter admits to
54 introduce infinitary objects in the typical LCF manner (e.g.\ lazy
55 lists). See also \cite{MuellerNvOS99} for a general discussion of