2 |
2 |
3 theory HOLCF_Specific |
3 theory HOLCF_Specific |
4 imports HOLCF |
4 imports HOLCF |
5 begin |
5 begin |
6 |
6 |
|
7 chapter {* HOLCF specific elements *} |
|
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 |
7 end |
59 end |