--- a/src/HOLCF/Stream.thy Thu Jun 29 16:16:24 1995 +0200
+++ b/src/HOLCF/Stream.thy Thu Jun 29 16:28:40 1995 +0200
@@ -62,40 +62,41 @@
(* stream_abs is an isomorphism with inverse stream_rep *)
(* identity is the least endomorphism on 'a stream *)
-stream_abs_iso "stream_rep[stream_abs[x]] = x"
-stream_rep_iso "stream_abs[stream_rep[x]] = x"
+stream_abs_iso "stream_rep`(stream_abs`x) = x"
+stream_rep_iso "stream_abs`(stream_rep`x) = x"
stream_copy_def "stream_copy == (LAM f. stream_abs oo
- (ssplit[LAM x y. x ## (lift[up oo f])[y]] oo stream_rep))"
-stream_reach "(fix[stream_copy])[x]=x"
+ (ssplit`(LAM x y. (|x , (lift`(up oo f))`y|) )) oo stream_rep)"
+stream_reach "(fix`stream_copy)`x = x"
+defs
(* ----------------------------------------------------------------------- *)
(* properties of additional constants *)
(* ----------------------------------------------------------------------- *)
(* constructors *)
-scons_def "scons == (LAM x l. stream_abs[x##up[l]])"
+scons_def "scons == (LAM x l. stream_abs`(| x, up`l |))"
(* ----------------------------------------------------------------------- *)
(* discriminator functional *)
stream_when_def
-"stream_when == (LAM f l.ssplit[LAM x l.f[x][lift[ID][l]]][stream_rep[l]])"
+"stream_when == (LAM f l.ssplit `(LAM x l.f`x`(lift`ID`l)) `(stream_rep`l))"
(* ----------------------------------------------------------------------- *)
(* discriminators and selectors *)
-is_scons_def "is_scons == stream_when[LAM x l.TT]"
-shd_def "shd == stream_when[LAM x l.x]"
-stl_def "stl == stream_when[LAM x l.l]"
+is_scons_def "is_scons == stream_when`(LAM x l.TT)"
+shd_def "shd == stream_when`(LAM x l.x)"
+stl_def "stl == stream_when`(LAM x l.l)"
(* ----------------------------------------------------------------------- *)
(* the taker for streams *)
-stream_take_def "stream_take == (%n.iterate(n,stream_copy,UU))"
+stream_take_def "stream_take == (%n.iterate n stream_copy UU)"
(* ----------------------------------------------------------------------- *)
-stream_finite_def "stream_finite == (%s.? n.stream_take(n)[s]=s)"
+stream_finite_def "stream_finite == (%s.? n.stream_take n `s=s)"
(* ----------------------------------------------------------------------- *)
(* definition of bisimulation is determined by domain equation *)
@@ -103,9 +104,9 @@
stream_bisim_def "stream_bisim ==
(%R.!s1 s2.
- R(s1,s2) -->
+ R s1 s2 -->
((s1=UU & s2=UU) |
- (? x s11 s21. x~=UU & s1=scons[x][s11] & s2 = scons[x][s21] & R(s11,s21))))"
+ (? x s11 s21. x~=UU & s1=scons`x`s11 & s2 = scons`x`s21 & R s11 s21)))"
end