author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 14535 | 7cb26928e70d |
child 15188 | 9d57263faf9e |
permissions | -rw-r--r-- |
11348 | 1 |
(* Title: HOLCF/ex/Stream.thy |
9169 | 2 |
ID: $Id$ |
2570 | 3 |
Author: Franz Regensburger, David von Oheimb |
4 |
||
12036 | 5 |
General Stream domain. |
14535
7cb26928e70d
added Streams.thy (with stream concatenation etc.)
oheimb
parents:
14171
diff
changeset
|
6 |
TODO: should be integrated with HOLCF/Streams |
2570 | 7 |
*) |
8 |
||
11348 | 9 |
Stream = HOLCF + Nat_Infinity + |
2570 | 10 |
|
4122 | 11 |
domain 'a stream = "&&" (ft::'a) (lazy rt::'a stream) (infixr 65) |
2570 | 12 |
|
11348 | 13 |
consts |
14 |
||
12036 | 15 |
smap :: "('a -> 'b) -> 'a stream -> 'b stream" |
16 |
sfilter :: "('a -> tr) -> 'a stream -> 'a stream" |
|
17 |
slen :: "'a stream => inat" ("#_" [1000] 1000) |
|
11348 | 18 |
|
19 |
defs |
|
20 |
||
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
12036
diff
changeset
|
21 |
smap_def "smap == fix\\<cdot>(\\<Lambda> h f s. case s of x && xs => f\\<cdot>x && h\\<cdot>f\\<cdot>xs)" |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
12036
diff
changeset
|
22 |
sfilter_def "sfilter == fix\\<cdot>(\\<Lambda> h p s. case s of x && xs => |
11348 | 23 |
If p\\<cdot>x then x && h\\<cdot>p\\<cdot>xs else h\\<cdot>p\\<cdot>xs fi)" |
12036 | 24 |
slen_def "#s == if stream_finite s |
11348 | 25 |
then Fin (LEAST n. stream_take n\\<cdot>s = s) else \\<infinity>" |
26 |
||
2570 | 27 |
end |
28 |
||
29 |