60 (* functor term: FT = <**,K_{'a},U> *) |
60 (* functor term: FT = <**,K_{'a},U> *) |
61 (* ----------------------------------------------------------------------- *) |
61 (* ----------------------------------------------------------------------- *) |
62 (* stream_abs is an isomorphism with inverse stream_rep *) |
62 (* stream_abs is an isomorphism with inverse stream_rep *) |
63 (* identity is the least endomorphism on 'a stream *) |
63 (* identity is the least endomorphism on 'a stream *) |
64 |
64 |
65 stream_abs_iso "stream_rep[stream_abs[x]] = x" |
65 stream_abs_iso "stream_rep`(stream_abs`x) = x" |
66 stream_rep_iso "stream_abs[stream_rep[x]] = x" |
66 stream_rep_iso "stream_abs`(stream_rep`x) = x" |
67 stream_copy_def "stream_copy == (LAM f. stream_abs oo |
67 stream_copy_def "stream_copy == (LAM f. stream_abs oo |
68 (ssplit[LAM x y. x ## (lift[up oo f])[y]] oo stream_rep))" |
68 (ssplit`(LAM x y. (|x , (lift`(up oo f))`y|) )) oo stream_rep)" |
69 stream_reach "(fix[stream_copy])[x]=x" |
69 stream_reach "(fix`stream_copy)`x = x" |
70 |
70 |
|
71 defs |
71 (* ----------------------------------------------------------------------- *) |
72 (* ----------------------------------------------------------------------- *) |
72 (* properties of additional constants *) |
73 (* properties of additional constants *) |
73 (* ----------------------------------------------------------------------- *) |
74 (* ----------------------------------------------------------------------- *) |
74 (* constructors *) |
75 (* constructors *) |
75 |
76 |
76 scons_def "scons == (LAM x l. stream_abs[x##up[l]])" |
77 scons_def "scons == (LAM x l. stream_abs`(| x, up`l |))" |
77 |
78 |
78 (* ----------------------------------------------------------------------- *) |
79 (* ----------------------------------------------------------------------- *) |
79 (* discriminator functional *) |
80 (* discriminator functional *) |
80 |
81 |
81 stream_when_def |
82 stream_when_def |
82 "stream_when == (LAM f l.ssplit[LAM x l.f[x][lift[ID][l]]][stream_rep[l]])" |
83 "stream_when == (LAM f l.ssplit `(LAM x l.f`x`(lift`ID`l)) `(stream_rep`l))" |
83 |
84 |
84 (* ----------------------------------------------------------------------- *) |
85 (* ----------------------------------------------------------------------- *) |
85 (* discriminators and selectors *) |
86 (* discriminators and selectors *) |
86 |
87 |
87 is_scons_def "is_scons == stream_when[LAM x l.TT]" |
88 is_scons_def "is_scons == stream_when`(LAM x l.TT)" |
88 shd_def "shd == stream_when[LAM x l.x]" |
89 shd_def "shd == stream_when`(LAM x l.x)" |
89 stl_def "stl == stream_when[LAM x l.l]" |
90 stl_def "stl == stream_when`(LAM x l.l)" |
90 |
91 |
91 (* ----------------------------------------------------------------------- *) |
92 (* ----------------------------------------------------------------------- *) |
92 (* the taker for streams *) |
93 (* the taker for streams *) |
93 |
94 |
94 stream_take_def "stream_take == (%n.iterate(n,stream_copy,UU))" |
95 stream_take_def "stream_take == (%n.iterate n stream_copy UU)" |
95 |
96 |
96 (* ----------------------------------------------------------------------- *) |
97 (* ----------------------------------------------------------------------- *) |
97 |
98 |
98 stream_finite_def "stream_finite == (%s.? n.stream_take(n)[s]=s)" |
99 stream_finite_def "stream_finite == (%s.? n.stream_take n `s=s)" |
99 |
100 |
100 (* ----------------------------------------------------------------------- *) |
101 (* ----------------------------------------------------------------------- *) |
101 (* definition of bisimulation is determined by domain equation *) |
102 (* definition of bisimulation is determined by domain equation *) |
102 (* simplification and rewriting for abstract constants yields def below *) |
103 (* simplification and rewriting for abstract constants yields def below *) |
103 |
104 |
104 stream_bisim_def "stream_bisim == |
105 stream_bisim_def "stream_bisim == |
105 (%R.!s1 s2. |
106 (%R.!s1 s2. |
106 R(s1,s2) --> |
107 R s1 s2 --> |
107 ((s1=UU & s2=UU) | |
108 ((s1=UU & s2=UU) | |
108 (? x s11 s21. x~=UU & s1=scons[x][s11] & s2 = scons[x][s21] & R(s11,s21))))" |
109 (? x s11 s21. x~=UU & s1=scons`x`s11 & s2 = scons`x`s21 & R s11 s21)))" |
109 |
110 |
110 end |
111 end |
111 |
112 |
112 |
113 |
113 |
114 |