26840
|
1 |
(* $Id$ *)
|
|
2 |
|
|
3 |
theory HOLCF_Specific
|
|
4 |
imports HOLCF
|
|
5 |
begin
|
|
6 |
|
26852
|
7 |
chapter {* Isabelle/HOLCF \label{ch:holcf} *}
|
26841
|
8 |
|
|
9 |
section {* Mixfix syntax for continuous operations *}
|
|
10 |
|
|
11 |
text {*
|
|
12 |
\begin{matharray}{rcl}
|
|
13 |
@{command_def (HOLCF) "consts"} & : & \isartrans{theory}{theory} \\
|
|
14 |
\end{matharray}
|
|
15 |
|
|
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
|
|
20 |
x"}.
|
|
21 |
|
|
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!
|
|
29 |
*}
|
|
30 |
|
|
31 |
|
|
32 |
section {* Recursive domains *}
|
|
33 |
|
|
34 |
text {*
|
|
35 |
\begin{matharray}{rcl}
|
|
36 |
@{command_def (HOLCF) "domain"} & : & \isartrans{theory}{theory} \\
|
|
37 |
\end{matharray}
|
|
38 |
|
|
39 |
\begin{rail}
|
|
40 |
'domain' parname? (dmspec + 'and')
|
|
41 |
;
|
|
42 |
|
|
43 |
dmspec: typespec '=' (cons + '|')
|
|
44 |
;
|
|
45 |
cons: name (type *) mixfix?
|
|
46 |
;
|
|
47 |
dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
|
|
48 |
\end{rail}
|
|
49 |
|
|
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
|
|
56 |
HOLCF domains.
|
|
57 |
*}
|
|
58 |
|
26840
|
59 |
end
|