author | wenzelm |
Thu, 12 Mar 2009 00:02:03 +0100 | |
changeset 30462 | 0b857a58b15e |
parent 30168 | 9a20be5be90b |
child 42596 | 6c621a9d612a |
permissions | -rw-r--r-- |
26840 | 1 |
theory HOLCF_Specific |
2 |
imports HOLCF |
|
3 |
begin |
|
4 |
||
26852 | 5 |
chapter {* Isabelle/HOLCF \label{ch:holcf} *} |
26841 | 6 |
|
7 |
section {* Mixfix syntax for continuous operations *} |
|
8 |
||
9 |
text {* |
|
10 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
26852
diff
changeset
|
11 |
@{command_def (HOLCF) "consts"} & : & @{text "theory \<rightarrow> theory"} \\ |
26841 | 12 |
\end{matharray} |
13 |
||
14 |
HOLCF provides a separate type for continuous functions @{text "\<alpha> \<rightarrow> |
|
15 |
\<beta>"}, with an explicit application operator @{term "f \<cdot> x"}. |
|
16 |
Isabelle mixfix syntax normally refers directly to the pure |
|
17 |
meta-level function type @{text "\<alpha> \<Rightarrow> \<beta>"}, with application @{text "f |
|
18 |
x"}. |
|
19 |
||
20 |
The HOLCF variant of @{command (HOLCF) "consts"} modifies that of |
|
21 |
Pure Isabelle (cf.\ \secref{sec:consts}) such that declarations |
|
22 |
involving continuous function types are treated specifically. Any |
|
23 |
given syntax template is transformed internally, generating |
|
24 |
translation rules for the abstract and concrete representation of |
|
25 |
continuous application. Note that mixing of HOLCF and Pure |
|
26 |
application is \emph{not} supported! |
|
27 |
*} |
|
28 |
||
29 |
||
30 |
section {* Recursive domains *} |
|
31 |
||
32 |
text {* |
|
33 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
26852
diff
changeset
|
34 |
@{command_def (HOLCF) "domain"} & : & @{text "theory \<rightarrow> theory"} \\ |
26841 | 35 |
\end{matharray} |
36 |
||
37 |
\begin{rail} |
|
38 |
'domain' parname? (dmspec + 'and') |
|
39 |
; |
|
40 |
||
41 |
dmspec: typespec '=' (cons + '|') |
|
42 |
; |
|
43 |
cons: name (type *) mixfix? |
|
44 |
; |
|
45 |
dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs |
|
46 |
\end{rail} |
|
47 |
||
48 |
Recursive domains in HOLCF are analogous to datatypes in classical |
|
49 |
HOL (cf.\ \secref{sec:hol-datatype}). Mutual recursion is |
|
50 |
supported, but no nesting nor arbitrary branching. Domain |
|
51 |
constructors may be strict (default) or lazy, the latter admits to |
|
52 |
introduce infinitary objects in the typical LCF manner (e.g.\ lazy |
|
53 |
lists). See also \cite{MuellerNvOS99} for a general discussion of |
|
54 |
HOLCF domains. |
|
55 |
*} |
|
56 |
||
26840 | 57 |
end |