1 (* Title: HOLCF/ex/Stream.thy |
1 (* Title: HOLCF/ex/Stream.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger, David von Oheimb |
3 Author: Franz Regensburger, David von Oheimb |
4 Copyright 1993, 1995 Technische Universitaet Muenchen |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 |
5 |
6 general Stream domain |
6 General Stream domain. |
7 *) |
7 *) |
8 |
8 |
9 Stream = HOLCF + Nat_Infinity + |
9 Stream = HOLCF + Nat_Infinity + |
10 |
10 |
11 domain 'a stream = "&&" (ft::'a) (lazy rt::'a stream) (infixr 65) |
11 domain 'a stream = "&&" (ft::'a) (lazy rt::'a stream) (infixr 65) |
12 |
12 |
13 consts |
13 consts |
14 |
14 |
15 smap :: "('a \\<rightarrow> 'b) \\<rightarrow> 'a stream \\<rightarrow> 'b stream" |
15 smap :: "('a -> 'b) -> 'a stream -> 'b stream" |
16 sfilter :: "('a \\<rightarrow> tr) \\<rightarrow> 'a stream \\<rightarrow> 'a stream" |
16 sfilter :: "('a -> tr) -> 'a stream -> 'a stream" |
17 slen :: "'a stream \\<Rightarrow> inat" ("#_" [1000] 1000) |
17 slen :: "'a stream => inat" ("#_" [1000] 1000) |
18 |
18 |
19 defs |
19 defs |
20 |
20 |
21 smap_def "smap \\<equiv> fix\\<cdot>(\\<Lambda>h f s. case s of x && xs => f\\<cdot>x && h\\<cdot>f\\<cdot>xs)" |
21 smap_def "smap == fix\\<cdot>(\\<Lambda>h f s. case s of x && xs => f\\<cdot>x && h\\<cdot>f\\<cdot>xs)" |
22 sfilter_def "sfilter \\<equiv> fix\\<cdot>(\\<Lambda>h p s. case s of x && xs => |
22 sfilter_def "sfilter == fix\\<cdot>(\\<Lambda>h p s. case s of x && xs => |
23 If p\\<cdot>x then x && h\\<cdot>p\\<cdot>xs else h\\<cdot>p\\<cdot>xs fi)" |
23 If p\\<cdot>x then x && h\\<cdot>p\\<cdot>xs else h\\<cdot>p\\<cdot>xs fi)" |
24 slen_def "#s \\<equiv> if stream_finite s |
24 slen_def "#s == if stream_finite s |
25 then Fin (LEAST n. stream_take n\\<cdot>s = s) else \\<infinity>" |
25 then Fin (LEAST n. stream_take n\\<cdot>s = s) else \\<infinity>" |
26 |
26 |
27 end |
27 end |
28 |
28 |
29 |
29 |